SatSolver Module
This module implements functions for checking the satisfiability of boolean expressions. The SAT checking procedures are based on Shannon graphs which are unreduced unordered binary decision diagrams. This has the advantage that one can construct an equivalent Shannon graph for a given BoolExpr in linear time.
Types
| Type | Description |
AtomIndex is used to uniquely identify atomic formulas (see maps Index2BoolExpr and BoolExpr2Index) |
|
|
a clause consists of a pair of sets of atom indices that are the indices of the positive and negative atoms of the clause; note that these are implicitly disjunctively combined and clauses are often used in combination with a cube that filters out only unassigned atoms |
|
|
ClauseIndex is used as type for indices of clauses in the ClauseArray |
|
|
A cube is a type to define a truth assignments to the considered atoms such that each atom is either true, false or don't care (=None). Cubes are ordered in a lattice. |
|
|
Shannon graphs are unreduced and unordered binary decision diagrams. Additionally, we add negations to allow a linear representation of equivalences. |
Functions and values
| Function or value | Description |
|
Given a BoolExpr phi, BoolExpr2Clauses phi computes (vrs,atoms,cls) where vrs are the variables (as BoolExprs) that where used to abbreviate subformulas occurring in phi into clauses, atoms is a set of atom indices including all atoms that occur in the clauses (i.e., vrs Abbreviated variables have names starting with "__def".
|
|
|
mapping boolean expressions to their index |
|
convert a BoolExpr to a Shannon graph (it is assumed that the atoms of e are at least a subset of the atom set used with Initialize)
|
|
convert a clause to a string
|
|
DPLL is the famous Davis-Putnam-Logemann-Loveland algorithm to check the satisfiability of an array of clauses over a set of atoms atomSet. Given clauses clauseArr over the atoms in atomSet, the procedure searches a satisfying assignment of the clause set. Argument numClauses partitions the clauses of the clause array into original clauses clauseArr[0..numClauses-1] and learnt ones due to a previous run of DPLL. Searching a model is done by the DPLL procedure by case splitting and unit propagation until a model or a conflict is found. Conflicts are used to learn a clause that avoids that the same conflict is repeated and that allows one to backtrack sometimes to higher decision levels. This implementation of DPLL computes for each found conflict of a branch a single assertion clause, and learns the one that leads to the largest backtrack step. The procedure returns a tuple (ca,nc,copt) where ca is the given clause array extended by learnt clauses, nc is still the number of original clauses, and copt is None if the set of clauses is unsatisfiable, and otherwise, it contains a cube that satisfies the given clause set. Arguments quite, write, and debug are used to determine whether notes on the computation are printed by the function write. If quiet holds, nothing is printed, otherwise some information is printed, and more information is printed when quiet is false and debug is true. |
|
|
Index2BoolExpr maps node indices to the corresponding boolean expression
|
|
Initialize the package by a set of boolean atoms. This set can e.g. be computed by AtomsOfBoolExpr from a BoolExpr. |
|
This function continues with a previous DPLL search that computed the result (ds,ats,ca,nc,mold) as described by function OneSatDPLL. The result is also as described there, just containing another model or the information that no more model exists. |
|
|
This function translates the given BoolExpr phi to a clause set, and runs DPLL with the arguments quiet, write, and debug as described with function DPLL. It returns a tuple (ds,ats,ca,m) where ds is the final decision stack (the final branch in the search tree), ats the set of atoms contained in phi, ca the clause array generated from phi as well as of the learnt clauses
|
|
|
|
write a Shannon graph to a dot file
|
|
print a variable assignment (a cube)
|