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*.
*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).
*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)

Logic Programming with Satisfiability; Michael Codish, Vitaly Lagoon and Peter Stuckey.

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

- MiniSat v2.0.2 by Niklas Een, Niklas Sorensson
- CryptoMiniSat v2.5.1 by Mate Soos
- Glucose v2.2 by Gilles Audemard, Laurent Simon
- Glucose v4.0 by Gilles Audemard, Laurent Simon

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]]].

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).

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

**sat(Cnf)****satMinUnary(Cnf,Unary)**- bind the*Cnf*variables to truth values that satisfy*Cnf*and minimize the value of the number*Unary*(*Unary*is a list of literals representing a number in order encoding - leading ones)**satMaxUnary(Cnf,Unary)**- bind the*Cnf*variables to truth values that satisfy*Cnf*and maximize the value of the number*Unary*(*Unary*is a list of literals representing a number in order encoding - leading ones)**satMinBinary(Cnf,Binary)**- bind the*Cnf*variables to truth values that satisfy*Cnf*and minimize the value of the number*Binary*(*Binary*is a list of literals representing a number in binary encoding - Most Significant Bit first)

If the formula

(Each of the above predicates using the corresponding predicates from the next list while ignoring the

**sat(Cnf,Solved,Time)****satMinUnary(Cnf,Unary,Solved,RunTime)****satMaxUnary(Cnf,Unary,Solved,RunTime)****satMinBinary(Cnf,Binary,Solved,RunTime)**

If the formula

**satMulti(Cnf,MaxSols,SolCount,Time)**

- The Prolog interface tested with the following SWI-Prolog version 6.6.6 and 7.2.3.
- When using Windows the SAT solvers libary files are .dll files instead of .so files.

- Source Code
- For SWI-Prolog 6.6.6 Windows 32 bits (compiled using MinGW)
- For SWI-Prolog 7.2.3 Windows 32 bits (compiled using MinGW)
- Other version of SWI-Prolog and/or Linux - download the source code and compile.