ZAT is a simple SAT solver implemented in zig.
- zig == 0.14.0
Use zig build to build zat preferably with -Dno-assert=true which removes larger
assertions.
just call:
./zat path/to/instance.cnfZAT does almost have no features (for a SAT solver). The Features include:
- a simple CDCL implementation.
- eVSIDS and Phase Saving for choosing variables
- Unit propagation using 2 watched literals.
- Parsing DIMACS
*.cnffiles and using the standard Protocol for SAT solvers. - (Not really a feature) no clause deletion algorithm.