In the context of Prof. Vardi COMP 509 Logic class at Rice University, I have developed a DPLL SAT Solver in Java that I hope you will enjoy!

The DPLL SAT Solver is based on an interative implementation of the DPLL design and currently supports 3 heuristics for the Splitting rule:

• Random Choice
• Two Clauses
• Jeroslow-Wang

(back to top)

• Java 17

Here is an example of usage to run the solver with the RandomChoice heuristics over a DIMACS-formatted file test.cnf:

java -jar Solver.jar test.cnf RandomChoice

(back to top)

Alexis Le Glaunec - alexis.leglaunec@rice.edu

(back to top)