funsat-0.5.2: A modern DPLL-style SAT solver




Data types used when dealing with SAT problems in funsat.


Basic Types

newtype Var Source




unVar :: Int

inLit :: (Int -> Int) -> Lit -> LitSource

litSign :: Lit -> BoolSource

The polarity of the literal. Negative literals are false; positive literals are true. The 0-literal is an error.

var :: Lit -> VarSource

The variable for the given literal.

type Clause = [Lit]Source

data CNF Source




class Ord a => Setlike t a whereSource

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.


without :: t -> a -> tSource

The set-like object with an element removed.

with :: t -> a -> tSource

The set-like object with an element included.

contains :: t -> a -> BoolSource

Whether the set-like object contains a certain element.


Setlike IAssignment Lit 
Ord a => Setlike [a] a 
(Ord a, Hash a) => Setlike (BitSet a) a 
Ord a => Setlike (Set a) a 
(Ord k, Ord a) => Setlike (Map k a) (k, a) 


type IAssignment = UArray Var IntSource

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.

type MAssignment s = STUArray s Var IntSource

Mutable array corresponding to the IAssignment representation.

freezeAss :: MAssignment s -> ST s IAssignmentSource

Same as freeze, but at the right type so GHC doesn't yell at me.

assign :: MAssignment s -> Lit -> ST s (MAssignment s)Source

Destructively update the assignment with the given literal.

unassign :: MAssignment s -> Lit -> ST s (MAssignment s)Source

Destructively undo the assignment to the given literal.

litAssignment :: IAssignment -> [Lit]Source

The assignment as a list of signed literals.

data Cut f gr a b Source

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




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


(Show (f Node), Show (gr a b)) => Show (Cut f gr a b) 

data CGNodeAnnot Source

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.


CGNA Lit Int 



class Model a m whereSource

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.


statusUnder :: a -> m -> Either () BoolSource

x `statusUnder` m should use Right if the status of x is defined, and Left otherwise.

Internal data types

type LevelArray s = STUArray s Var LevelSource

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.

type FrozenLevelArray = UArray Var LevelSource

Immutable version.

newtype VarOrder s Source

The VSIDS-like dynamic variable ordering.




type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId)Source

Each pair of watched literals is paired with its clause and id.