slow-cdcl

Yet another inefficient and slow SMT solver using a slow and inefficient hand crafted CDCL solver and using z3 as a theory solver

Dev Env Setup

• Python <= 3.10 (assumes virtualenv pyenv etc. is install)

$ virtualenv -p python cdcl-env
$ source cdcl-env/bin/activate
$ pip install -r requirements.txt
$ pysmt-install --z3

• check installation

$ python -i example.py

• run

python main.py <filename>

Tests

• in the tests folder

Tasks

1. Build a CDCL solver
   • Use an appropriate term representation of propositional logic.
   • Use the appropriate translation of the logic rules to come up with an assignment
2. Interface the CDCL solver with the LIA theory formulas
3. Parse the smt-lib2 files and store them in an appropriate AST
4. Convert them to a Propositional logic formula
5. ask the CDCL solver if an assigment is possible
   • If it is satisfiable send it to the theory solver to come up with an assigment or output unsat
6. come up with an unsat core using z3

Notes:

• Allowed to refer https://kienyew.github.io/CDCL-SAT-Solver-from-Scratch/, but if we do that, we have to add our own enhancements such as:
  • the Variable State Independent Decaying Sum (VSIDS) heuristic, to pick an unassigned variable for Decide;
  • a Luby policy, or an arithmetic policy for Restart;
  • a time and space-efficient implementation using Numpy arrays instead of less efficient implementations such as dictionaries or maps.

Input

• https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
• pySMT to parse - http://www.pysmt.org/

Output

Bunch of debug messages. Final message is sat or unsat In case of sat, a model is printed

perf-stats.txt shows performance stats