A SAT Solver based on CDCL (Conflict Driven Clause Learning) implemented in Python.
SAT is the satisfiability problem wherein we are given some clauses containing propositional variables and the correspoding literals and we need to find whether the formula is satisfiable or unsatisfiable. A SAT Solver is a program that solves a SAT problem. Most of the state-of-the-art SAT solvers nowadays use the CDCL (Conflict Driven Clause Learning) algorithm to implement the solver.
The contents of this folder and how to use them:
- Images folder: An image included in the Jupyter notebook describing the Luby Sequence.
- test folder: It has the test cases (SAT problems in DIMACS CNF format).
- Results folder: Statistics and assignments produced by the solver when run on the examples from the test folder.
- LubyGenerator.py file: Methods to generate Luby Sequence (used internally by the solver).
- PriorityQueue.py file: Methods to implement the PriorityQueue (used internally by the solver).
- SAT.ipynb file: The Jupyter notebook containing the solver's code and complete documentation. The notebook is accessed by starting the jupyter server by typing "jupyter notebook" in the terminal of this folder. This notebook has the whole code and all the examples at last. These examples can be run by executing the cells.
- SAT.py file: Python copy of the SAT.ipynb notebook.
- solver.py file: Uses SAT.py file to run the solver from the terminal. Use:
python3 solver.py <to_log> <decider> <restarter> <inputfile>
in the terminal where to_log must be True or False, decider must be ORDERED, MINISAT or VSIDS, restarter must be None, GEOMETRIC or LUBY and inputfile should be a valid path to the input file which has the SAT problem in DIMACS CNF format.
For eg.
python3 solver.py False MINISAT None test/sat/bmc-2.cnf
- verifier.py file: Checks if the assignment generated by the solver is indeed a valid assignment. Use:
python3 verifier.py <inputfile> <assignmentfile>
in the terminal where, inputfile should be a valid path to the input file which has the SAT problem in DIMACS CNF format (eg. test/sat/bmc-1.cnf) and assignmentfile should be valid path to the assignmentfile generated by the solver (eg. Result/assgn_bmc-1.cnf).