PL-CryptoMinisat is now part of PL-SATsolver.

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)

## Notes

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