Pure Kotlin high performance implementation of Binary Decision Diagrams. Can be used as:

• Kotlin/Java library via API

• Command Line Interface as SAT solver that takes standard input and produces standard output as specified SAT competitions format

# java -jar kobdd-0.1.jar
v KOBDD SAT SOLVER, v0.1
v Solves formulas in CNF form. Input must as formatted according simplified DIMACS specified in http://www.satcompetition.org/2004/format-solvers2004.html


c REQUEST
c 
c comments
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0


v Start processing CNF request with 5 variables and 3 clauses
v processed clause [1, -5, 4]
v processed clause [-1, 5, 3, 4]
v processed clause [-3, -4]
v Request processed in 0.039 sec
s SATISFIABLE
v 1 3 -4
c Done

One of the goals for SAT-solver based on BDD is to show that it can solve PHP problem unsolvable by CDCL based SAT solver. Any CDCL solver works almost infinitely long for PHP(21,20) because it has to generate exponential size proof to validate that solution is UNSAT (The intractability of resolution, Armin Haken, Theoretical Computer Science Volume 39, 1985, Pages 297-308).

For BDD-based solver it was shown that polynomial proof exists in A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77–91. Later direct algorithm with proven polynomial complexity was proposed in A direct construction of polynomial-size OBDD proof of pigeon hole problem, Wěi Chén, Wenhui Zhang, Information Processing Letters Volume 109, Issue 10, 30 April 2009, Pages 472-477

In this repository the algorithm is implemented using KOBDD solver and can be verified by running tests in TestPhp class. Following experimental results for PHP(n+1,n) were obtained on Intel Core i7-8550U, 1.8GHz 16GB RAM:

For comparison quite efficient Minisat CDCL-based solver works 3.5 sec for PHP(10,9), 197 sec for PHP(11,10) and too long to wait for PHP(12,11) on the same machine.