Final project for CPSC 454/554 Software Analytics & Varification at Yale, 2015 Fall
It is a C++ implementation of Chaff SAT solver.
A makefile is contained in this project, please type following command in the terminal to compile it.
make
(It is tested in yale zoo environment.)
- Basic Davis-Putnam Backtrack Search
- Optimized BCP
- Variable State Independent Decaying Sum(VSIDS) Decision Heuristic
CNF format
For more information about CNF format please visit http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html
Chaff: Engineering an Efficient SAT Solver
Bo Song, Keshan Liu