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?

  • 6
    $\begingroup$ 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. $\endgroup$ Jul 16 '21 at 21:16

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.