A basic SAT solver that implements the standard DPLL algorithm with a slightly modified unit propagation algorithm described in the paper by Crawford & Auton. The solver expects problems to be already in the conjunctive normal form (CNF) and accepts DIMACS files as input and will print the result to STDOUT as described in the DIMACS specification. Some test inputs are available in the resources directory - some of which are sourced from the SATLIB benchmark problems.
Currently there is a CDCL solver in the works.
$ lein run resources/test.cnf
Copyright © 2020 Vipin Nair
This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 which is available at http://www.eclipse.org/legal/epl-2.0.
This Source Code may also be made available under the following Secondary Licenses when the conditions for such availability set forth in the Eclipse Public License, v. 2.0 are satisfied: GNU General Public License as published by the Free Software Foundation, either version 2 of the License, or (at your option) any later version, with the GNU Classpath Exception which is available at https://www.gnu.org/software/classpath/license.html.