If you look up the spec for CNF files then you will find that this is a pretty simple text format. Here is an (untested) Java code that parses a CNF file and translates it to a CPLEX model or LP file.
import ilog.cplex.IloCplex;
import ilog.concert.IloException;
import ilog.concert.IloIntVar;
import ilog.concert.IloLinearNumExpr;
import java.io.IOException;
import java.nio.charset.Charset;
import java.nio.file.Files;
import java.nio.file.Paths;
public final class ReadCnf {
public static void main(String[] args) throws IloException, IOException {
IloCplex cplex = new IloCplex();
try {
int vars = -1, clauses = -1;
IloIntVar[] x = null;
for (String line : Files.readAllLines(Paths.get(args[0]), Charset.forName("utf-8"))) {
if ( line.startsWith("c") )
// ignore comments
continue;
else if ( line.startsWith("p") ) {
// parse header
if ( vars >= 0 )
throw new IOException("Multiple headers");
String[] fields = line.split("\\s+");
if ( fields.length != 4 )
throw new IOException("Invalid header");
if ( !fields[1].equals("cnf") )
throw new IOException("Invalid format");
vars = Integer.parseInt(fields[2]);
clauses = Integer.parseInt(fields[3]);
x = cplex.boolVarArray(vars);
for (int i = 0; i < vars; ++i)
x[i].setName("x" + (i + 1));
}
else if ( line.startsWith("%") ) {
// Not sure what that means, just stop
break;
}
else {
// parse a clause
// note that in the file variables indices are 1-based while
// here they are 0-based.
IloLinearNumExpr expr = cplex.linearNumExpr();
double rhs = 1.0;
for (final String s : line.trim().split("\\s+")) {
int var = Integer.parseInt(s);
if ( var > 0 ) {
expr.addTerm(1.0, x[var - 1]);
}
else if ( var < 0 ) {
// complemented variable, add (1-x) to the left-hand
// side
expr.addTerm(-1, x[-var - 1]);
rhs -= 1.0;
}
else {
// 0 terminates a clause
break;
}
}
cplex.addGe(expr, rhs);
}
}
cplex.exportModel(args[1]);
//cplex.solve();
}
finally {
cplex.end();
}
}
}
Note that this is more flexible than what Alex suggested since it directly consumes the CNF file (including comments and header) and also is not limited to clauses of length 3.
#CPLEXOptimizers#DecisionOptimization