Adding clauses directly to the z3 solver

Question

I have an AIG (and-inverter graph) which I keep modifying and whose satisfiability I need to check in an incremental manner using Z3. I can generate a CNF representation of the AIG and would ideally like to feed these clauses directly to the solver and call it repeatedly from my code. Is there some way that I can directly add clauses (or an AIG) to Z3 solver through C/C++ APIs?

Answer 1

Yes, you can simply assert new assertions, which are internally translated into clauses.

Note that for many incremental solving problems, Z3 does not use an off-the-shelf, dedicated SAT-solver, but it's own SMT solver that incorporates some of the features of SAT solvers, but not all, and which natively handles non-Boolean problems. So, it's not necessarily the case that hacking the solver to inject clauses directly will translate into significantly improved performance.

Z3 also has a dedicated Boolean-only SAT solver and if you're solving purely Boolean problems, this solver is likely much faster. You can force it to use this solver by replacing (check-sat) with (check-sat-using sat), or by running the tactic called 'sat'. The implementation of this solver is in sat_solver.h/.cpp, which would be the prime place to start looking around, if you'd like to hack it.

Z3 also uses it's own implementation of AIGs as a pre-processing step in some tactics, see aig_tactic.h/.cpp.