Funsat.Types

Contents

Description

Data types used when dealing with SAT problems in funsat.

Synopsis

Basic Types

Constructors

V
Fields unVar :: Int

Instances

Enum Var
Eq Var
Num Var
Ord Var
Show Var
Ix Var
Hash Var
Model Var IAssignment
Show (STUArray s Var Double)
Show (STUArray s Var Int)

newtype Lit Source

Constructors

L
Fields unLit :: Int

Instances

Enum Lit
Eq Lit
Num Lit
Ord Lit
Read Lit
Show Lit
Ix Lit
Hash Lit
Model Lit IAssignment
Setlike IAssignment Lit
Error (Lit, Clause, ClauseId)

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

Transform the number inside the literal.

litSign :: Lit -> Bool Source

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

var :: Lit -> Var Source

The variable for the given literal.

lit :: Var -> Lit Source

The positive literal for the given variable.

type Clause = [Lit]Source

data CNF Source

Constructors

CNF
Fields numVars :: Int numClauses :: Int clauses :: Set Clause

Instances

Eq CNF
Read CNF
Show CNF

data Solution Source

The solution to a SAT problem. In each case we return an assignment, which is obviously right in the Sat case; in the Unsat case, the reason is to assist in the generation of an unsatisfiable core.

Constructors

Sat IAssignment
Unsat IAssignment

Instances

Eq Solution
Show Solution

finalAssignment :: Solution -> IAssignment 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.

Methods

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 -> Bool Source

Whether the set-like object contains a certain element.

Instances

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)

Assignments

type IAssignment = UArray Var Int Source

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.

showAssignment :: IAssignment -> String Source

type MAssignment s = STUArray s Var Int Source

Mutable array corresponding to the IAssignment representation.

freezeAss :: MAssignment s -> ST s IAssignment Source

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

unsafeFreezeAss :: MonadST s m => MAssignment s -> m IAssignment Source

See freezeAss.

thawAss :: IAssignment -> ST s (MAssignment s)Source

unsafeThawAss :: IAssignment -> ST s (MAssignment s)Source

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

Constructors

Cut
Fields 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

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

Constructors

CGNA Lit Int

Instances

Show CGNodeAnnot

Model

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.

Methods

statusUnder :: a -> m -> Either () Bool Source

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

Instances

Model Clause IAssignment
Model Lit IAssignment
Model Var IAssignment

Internal data types

type Level = Int Source

type LevelArray s = STUArray s Var Level Source

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 Level Source

Immutable version.

newtype VarOrder s Source

The VSIDS-like dynamic variable ordering.

Constructors

VarOrder
Fields varOrderArr :: STUArray s Var Double

Instances

Show (VarOrder s)

newtype FrozenVarOrder Source

Constructors

FrozenVarOrder (UArray Var Double)

Instances

Show FrozenVarOrder

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

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

type WatchArray s = STArray s Lit [WatchedPair s]Source

data PartialResolutionTrace Source

Constructors

PartialResolutionTrace
Fields resTraceIdCount :: !Int resTrace :: ![Int] resTraceOriginalSingles :: ![(Clause, ClauseId)] resSourceMap :: Map ClauseId [ClauseId]

Instances

Show PartialResolutionTrace

type ReasonMap = Map Var (Clause, ClauseId)Source

type ClauseId = Int Source