PL-SATsolver is a Prolog interface to "MiniSat based" SAT solver which is based on Prolog interface to the MiniSat described in the paper:
Logic Programming with Satisfiability; Michael Codish, Vitaly Lagoon and Peter Stuckey.

PL-SATsolver contains four SAT solvers with a single interface:

Prolog and CNF

A formula in conjunctive normal form is represented as a list of list of literals (a literal is a variable or its negation). The elements of the outer list are viewed as a conjunction. Each inner list is a disjunction.
For example the CNF formula (A+(-B))*((-A)+B) is represented as [[A,-B],[-A,B]]].
When using CrytoMiniSat, PL-SATsolver supports XOR clauses by adding the atom 'x' at the beginning of the clause list.
For example the CNF formula ((A xor B xor C)*(A+B)*((-B)+(-C))) is represented as [[x,A,B,C],[A,B],[-B,-C]]].

Usage

PL-SATsolver written and tested in SWI-Prolog and requires compilation of the SAT solver(s).
More details about compilation can be found at the README file in the package.
After retrieving PL-SATsolver files: satsolver.pl and (at least one of) pl-minisat.so / pl-crypminisat.so / pl-glucose.so / pl-glucose4.so and placing them in the same directory, execute Prolog and consult satsolver.pl. When consult satsolver.pl one of the SAT solvers will be loaded and pre-defined predicates will be available for use (see PL-SATsolver predicates bellow).

Consult Example #1

The default SAT solver is Glucose v2.2.
To use different SAT solver call 'nb_satval(satSolver_module,<value>)' before consulting 'satsolver.pl' where <value> can be: 'minisat', 'cryptominisat', 'glucose', or 'glucose4'.

Consult Example #2


PL-SATsolver predicates

The next predicates succeed if and only if the formula Cnf in conjunctive normal form is satisfiable. When succeed it binds Cnf variables to truth values 1 (true) and -1 (false) that satisfy Cnf. The next predicates always succeed and bind Time to the CPU time spend during the call to the predicate.
If the formula Cnf in conjunctive normal form is satisfiable then Solved bound to 1 and Cnf variables bound to trith values. Otherwise Solved bound to 0.
(Each of the above predicates using the corresponding predicates from the next list while ignoring the Time variable and using Solved as indication for succeess). The next predicate always succeed and bind Time to the CPU time spend during the call to the predicate.
If the formula Cnf in conjunctive normal form has k satisfying assignments then it binds each Cnf variable to a list of k truth values when the ith satisfying assignment is the ith element from each Cnf variable list. SolCount will be bound to the amount of satisfying assignments found (SolCount <= MaxSols).

Predicates Example


Notes


Downloads

Last updated (01/04/2016)