3

As I know, any SAT solver such as or-tools or cplex cp optimizer converts a given problem to CNF form in the first place. Is it possible to extract the resulting CNF representation from or-tools or cplex?

RobPratt
  • 32,006
  • 1
  • 44
  • 84
user856754
  • 39
  • 2
  • 6
    CPLEX CPO is not a SAT solver but a CP solver. To our knowledge, it does not convert the given model to CNF form. Google OR Tools CP-SAT solver is not a pure SAT solver as well. Roughly speaking, this is a CP solver that embeds SAT techniques as subroutines. The model is given following a CP formalism. – Hexaly Jul 16 '21 at 21:16

2 Answers2

5

CP-SAT uses a SAT backend. But at any moment, just like with SMT solvers, the full model is never fully represented using clauses and Boolean literals. I recommend looking at the CPAIOR 2020 masterclass on CP (on YouTube) to get a better understanding of the architecture of the solver.

Laurent Perron
  • 2,690
  • 1
  • 6
  • 18
3

Quick hack

  • Get glpk sources
  • Edit src/api/minisat1.c
  • Find
int glp_minisat1(glp_prob *P)
{     /* solve CNF-SAT problem with MiniSat solver */
      solver *s;
      GLPAIJ *aij;
  • Add one line
int glp_minisat1(glp_prob *P)
{     /* solve CNF-SAT problem with MiniSat solver */
      glp_write_cnfsat(P, "tmptmp.cnf");
      solver *s;
      GLPAIJ *aij;
  • Compile

./configure && make

  • Run

examples/glpsol --lp prob.lp --minisat

  • Quit solving with ctrl-c

Now you have tmptmp.cnf in the same directory.

user9050
  • 119
  • 5