JOHN - A Knowledge Representation Language

SAT (Satisfiability Solver)

Download:

sat.jmc

Overview:

This program is implements SAT solver as a planning problem, which is the reverse of what is common. Although it is not practical, this this program is a good way to learn about SAT problem and the DPLL? algorithm that solves it.

The SAT problem is expressed in Conjunctive Normal Form? (CNF) like the one below:

 
       -X1 + X3 + -X5
       -X2 + -X4 + X5
       -X1 + X2 + -X4
       -X3 + X4 + -X5
       X2 + X3 + -X4 + X5
       -X2 + -X3

which is expressed as follows in this program:

 
make Clause A [ X1n, X3p, X5n ].
make Clause B [ X2n, X4n, X5p ].
make Clause C [ X1n, X2p, X4n ].
make Clause D [ X3n, X4p, X5n ].
make Clause E [ X2p, X3p, X4n, X5p ].
make Clause F [ X2n, X3n ].

Sample Run

> SAT satisfy solve.
looking 1 time unit ahead (5 possible worlds)
looking 2 time unit ahead (20 possible worlds)
satisfied at time: 2
satisfied by: [ SAT falsify-indexed-variable 2 , SAT falsify-indexed-variable 0  ]
ok.

> all Variable.
[ X1, X2, X3, X4, X5 ]

> SAT cnf solution.
[ no, yes, no, yes, yes ]

Which means one model to the problem above is:

    X1 = F, X2 = T, X3 = F, X4 = T, X5 = T

• View
• Edit
• History
• Print