|
|
|
|
|
Description |
Data types used when dealing with SAT problems in funsat.
|
|
Synopsis |
|
|
|
|
Basic Types
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
|
|
The polarity of the literal. Negative literals are false; positive
literals are true. The 0-literal is an error.
|
|
|
The variable for the given literal.
|
|
|
|
|
Constructors | | Instances | |
|
|
|
Represents a container of type t storing elements of type a that
support membership, insertion, and deletion.
There are various data structures used in funsat which are essentially used
as ''set-like'' objects. I've distilled their interface into three
methods. These methods are used extensively in the implementation of the
solver.
| | Methods | | The set-like object with an element removed.
| | | The set-like object with an element included.
| | | Whether the set-like object contains a certain element.
|
| | Instances | |
|
|
Assignments
|
|
|
An ''immutable assignment''. Stores the current assignment according to
the following convention. A literal L i is in the assignment if in
location (abs i) in the array, i is present. Literal L i is absent
if in location (abs i) there is 0. It is an error if the location (abs
i) is any value other than 0 or i or negate i.
Note that the Model instance for Lit and IAssignment takes constant
time to execute because of this representation for assignments. Also
updating an assignment with newly-assigned literals takes constant time,
and can be done destructively, but safely.
|
|
|
Mutable array corresponding to the IAssignment representation.
|
|
|
Same as freeze, but at the right type so GHC doesn't yell at me.
|
|
|
See freezeAss.
|
|
|
|
|
|
|
Destructively update the assignment with the given literal.
|
|
|
Destructively undo the assignment to the given literal.
|
|
|
The assignment as a list of signed literals.
|
|
|
The union of the reason side and the conflict side are all the nodes in
the cutGraph (excepting, perhaps, the nodes on the reason side at
decision level 0, which should never be present in a learned clause).
| Constructors | Cut | | reasonSide :: f Node | The reason side contains at least the decision variables.
| conflictSide :: f Node | The conflict side contains the conflicting literal.
| cutUIP :: Node | | cutGraph :: gr a b | |
|
| Instances | |
|
|
|
Annotate each variable in the conflict graph with literal (indicating its
assignment) and decision level. The only reason we make a new datatype for
this is for its Show instance.
| Constructors | | Instances | |
|
|
Model
|
|
|
An instance of this class is able to answer the question, Is a
truth-functional object x true under the model m? Or is m a model
for x? There are three possible answers for this question: True (''the
object is true under m''), False (''the object is false under m''),
and undefined, meaning its status is uncertain or unknown (as is the case
with a partial assignment).
The only method in this class is so named so it reads well when used infix.
Also see: isTrueUnder, isFalseUnder, isUndefUnder.
| | Methods | | x `statusUnder` m should use Right if the status of x is
defined, and Left otherwise.
|
| | Instances | |
|
|
Internal data types
|
|
|
|
|
A level array maintains a record of the decision level of each variable
in the solver. If level is such an array, then level[i] == j means the
decision level for var number i is j. j must be non-negative when
the level is defined, and noLevel otherwise.
Whenever an assignment of variable v is made at decision level i,
level[unVar v] is set to i.
|
|
|
Immutable version.
|
|
|
The VSIDS-like dynamic variable ordering.
| Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Each pair of watched literals is paired with its clause and id.
|
|
|
|
data PartialResolutionTrace | Source |
|
Constructors | | Instances | |
|
|
|
|
|
|
Produced by Haddock version 2.3.0 |