PL-CryptoMinisat is now part of PL-SATsolver.

Please visit PL-SATsolver page.
PL-CryptoMinisat is a Prolog interface to the

CryptoMinisat 2.5.1 sat solver by Mate Soos which
is based on Prolog interface to the Minisat described in the paper:

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

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

PL-CryptoMinisat 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

After retrieving the two PL-CryptoMinisat files: crypminisat.pl and pl-crypminisat.so (or pl-crypminisat.dll)
from the Downloads section and placing them in the same directory, execute Prolog and consult crypminisat.pl.

## PL-CryptoMinisat 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*.

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

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

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

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

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

## Example

```
Unary=[A,B,C,D]
Cnf=[[A,-B],[B,-C],[C,-D],[A,B,Z],[D,C,-Z],[-A,-D]]
?- sat(Cnf).
Unary = [1, 1, -1, -1],
A = 1, B = 1,
C = -1, D = -1, Z = -1.
?- satMinUnary(Cnf,Unary).
Unary = [1, -1, -1, -1],
A = 1,
B = -1, C = -1, D = -1, Z = -1.
?- satMaxUnary(Cnf,Unary).
Unary = [1, 1, 1, -1],
A = 1, B = 1, C = 1,
D = -1, Z = -1.
?- satMulti(Cnf,5,Sols,_Time).
Sols=4,
Unary = [[1, 1, 1, 1], [1, -1, 1, 1], [1, -1, 1, -1], [-1, -1, -1, -1]],
A = [ 1, 1, 1, 1],
B = [ 1, -1, 1, 1],
C = [ 1, -1, 1, -1],
D = [-1, -1, -1, -1],
Z = [-1, -1, 1, -1].
```

## Notes

- The Prolog interface tested with the following SWI-Prolog versions: 5.8.3 and 6.0.2.

# Downloads

Last updated (17/08/2012)