How to convert SMT(containing boolean and bounded int variables) constraints to CNF

Question

My applicant is originally a SAT problem. Now, I'm trying to do some extension which requires to use some int variables. So the problem becomes a SMT problem. But I encountered a performance problem when using z3 to solve it. As the int variable is bounded (less than 100), it's viable to convert it to a pure SAT problem.

Does anyone know how to apply this tactic in z3 c++ interface? Or can I use z3 to convert the SMT constraints to SAT formulas firstly and then try other SAT solvers?
Thanks in advance.

Answer 1

If you represent your problem in a bit vector formula, e.g. QF_ABV, it will be automatically flattened into propositional formula, and solved using a SAT solver. For example, you can represent your less-than-100 integer variables as a bit vectors of 7 bits.

Apart from bit vector, conversion from SMT to SAT will not boost your performance (otherwise SMT would not exist). Because SAT solver is only good at case analysis, and theory-specific decision procedures, e.g. simplex-based algorithms for linear arithmetic, are much more efficient in constraint solving.

Answer 2

The yices SMT solver supports conversion from SMT constraints into SAT if Bitvectors are used. Use (export-to-dimacs "myfile.cnf") in SMT problem sheet and run yices with --logic=QF_BV option.