public static List<Formula> readCNF(final File file, final FormulaFactory f, final String prefix) throws IOException {
    final List<Formula> result = new ArrayList<>();
    try (final BufferedReader br = new BufferedReader(new FileReader(file))) {
      while (br.ready()) {
        final String line = br.readLine();
        if (!line.startsWith("c") && !line.startsWith("p") && !line.trim().isEmpty()) {
          final String[] split = line.split("\\s+");
          if (!"0".equals(split[split.length - 1].trim()))
            throw new IllegalArgumentException("Line " + line + " did not end with 0.");
          final LinkedHashSet<Literal> vars = new LinkedHashSet<>(split.length - 1);
          for (int i = 0; i < split.length - 1; i++) {
            final String lit = split[i].trim();
            if (!lit.isEmpty()) {
              if (lit.startsWith("-"))
                vars.add(f.literal(prefix + split[i].trim().substring(1), false));
              else
                vars.add(f.variable(prefix + split[i].trim()));
            }
          }
          result.add(f.or(vars));
        }
      }
    }
    return result;
  }
public static List < Formula > readCNF ( final File file , final FormulaFactory f , final String prefix ) throws IOException { final List < Formula > result = new ArrayList < > ( ) ; try ( final BufferedReader br = new BufferedReader ( new FileReader ( file ) ) ) { while ( br . ready ( ) ) { final String line = br . readLine ( ) ; if ( ! line . startsWith ( "c" ) && ! line . startsWith ( "p" ) && ! line . trim ( ) . isEmpty ( ) ) { final String [ ] split = line . split ( "\\s+" ) ; if ( ! "0" . equals ( split [ split . length - 1 ] . trim ( ) ) ) throw new IllegalArgumentException ( "Line " + line + " did not end with 0." ) ; final LinkedHashSet < Literal > vars = new LinkedHashSet < > ( split . length - 1 ) ; for ( int i = 0 ; i < split . length - 1 ; i ++ ) { final String lit = split [ i ] . trim ( ) ; if ( ! lit . isEmpty ( ) ) { if ( lit . startsWith ( "-" ) ) vars . add ( f . literal ( prefix + split [ i ] . trim ( ) . substring ( 1 ) , false ) ) ; else vars . add ( f . variable ( prefix + split [ i ] . trim ( ) ) ) ; } } result . add ( f . or ( vars ) ) ; } } } return result ; }
Reads a given DIMACS CNF file and returns the contained clauses as a list of formulas.
@param file   the file
@param f      the formula factory
@param prefix the prefix for the variable names
@return the list of formulas (clauses)
@throws IOException if there was a problem reading the file