SAT.Solver.Mios.Solver

This is a part of MIOS

Solver

data Solver

Fig. 2.(p.9) Internal State of the solver

Constructors

Solver

Fields

• model :: !VecBool

  If found, this vector has the model

• conflict :: !Stack

  set of literals in the case of conflicts Clause Database

• clauses :: !ClauseExtManager

  List of problem constraints.

• learnts :: !ClauseExtManager

  List of learnt clauses.

• watches :: !WatcherList

  a list of constraint wathing p, literal-indexed Assignment Management

• assigns :: !Vec

  The current assignments indexed on variables; var-indexed

• phases :: !Vec

  The last assignments indexed on variables; var-indexed

• trail :: !Stack

  List of assignments in chronological order; var-indexed

• trailLim :: !Stack

  Separator indices for different decision levels in trail.

• qHead :: !IntSingleton

  trail is divided at qHead; assignments and queue

• reason :: !ClauseVector

  For each variable, the constraint that implied its value; var-indexed

• level :: !Vec

  For each variable, the decision level it was assigned; var-indexed Variable Order

• activities :: !VecDouble

  Heuristic measurement of the activity of a variable; var-indexed

• order :: !VarHeap

  Keeps track of the dynamic variable order. Configuration

• config :: !MiosConfiguration

  search paramerters

• nVars :: !Int

  number of variables

• claInc :: !DoubleSingleton

  Clause activity increment amount to bump with. , varDecay :: !DoubleSingleton -- ^ used to set varInc

• varInc :: !DoubleSingleton

  Variable activity increment amount to bump with.

• rootLevel :: !IntSingleton

  Separates incremental and search assumptions. Working Memory

• ok :: !BoolSingleton

  return value holder

• an'seen :: !Vec

  scratch var for analyze; var-indexed

• an'toClear :: !Stack

  ditto

• an'stack :: !Stack

  ditto

• pr'seen :: !Vec

  used in propagate

• lbd'seen :: !Vec

  used in lbd computation

• lbd'key :: !IntSingleton

  used in lbd computation

• litsLearnt :: !Stack

  used to create a learnt clause

• lastDL :: !Stack

  last decision level used in analyze

• stats :: !Vec

  statistics information holder

Instances

VarOrder Solver

Interfate to select a decision var based on variable activity.

Methods

newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO Solver

newVar :: Solver -> IO Var

update :: Solver -> Var -> IO ()

updateAll :: Solver -> IO ()

undo :: Solver -> Var -> IO ()

select :: Solver -> IO Var

newSolver :: MiosConfiguration -> CNFDescription -> IO Solver

returns an everything-is-initialized solver from the arguments

Misc Accessors

nAssigns :: Solver -> IO Int

returns the number of current assigments

nClauses :: Solver -> IO Int

returns the number of constraints (clauses)

nLearnts :: Solver -> IO Int

returns the number of learnt clauses

decisionLevel :: Solver -> IO Int

returns the current decision level

valueVar :: Solver -> Var -> IO Int

returns the assignment (:: LiftedBool = [-1, 0, -1]) from Var

valueLit :: Solver -> Lit -> IO Int

returns the assignment (:: LiftedBool = [-1, 0, -1]) from Lit

locked :: Solver -> Clause -> IO Bool

Fig. 7. (p.11) returns True if the clause is locked (used as a reason). Learnt clauses only

data VarHeap

VarHeap is a heap tree built from two Vec This implementation is identical wtih that in Minisat-1.14 Note: the zero-th element of heap is used for holding the number of elements Note: VarHeap itself is not a VarOrder, because it requires a pointer to solver

State Modifiers

addClause :: Solver -> Vec -> IO Bool

returns False if a conflict has occured. This function is called only before the solving phase to register the given clauses.

enqueue :: Solver -> Lit -> Clause -> IO Bool

Fig. 9 (p.14) Puts a new fact on the propagation queue, as well as immediately updating the variable's value in the assignment vector. If a conflict arises, False is returned and the propagation queue is cleared. The parameter from contains a reference to the constraint from which p was propagated (defaults to Nothing if omitted).

assume :: Solver -> Lit -> IO Bool

Fig. 12 (p.17) returns False if immediate conflict.

Pre-condition: propagation queue is empty

cancelUntil :: Solver -> Int -> IO ()

#M22: Revert to the states at given level (keeping all assignment at level but not beyond).

getModel :: Solver -> IO [Int]

return the model as a list of literal

Activities

claBumpActivity :: Solver -> Clause -> IO ()

Fig. 14 (p.19)

claDecayActivity :: Solver -> IO ()

Fig. 14 (p.19)

varBumpActivity :: Solver -> Var -> IO ()

Fig. 14 (p.19) Bumping of clause activity

varDecayActivity :: Solver -> IO ()

Fig. 14 (p.19)

Stats

data StatIndex

stats

Constructors

NumOfBackjump

NumOfRestart

Instances

Bounded StatIndex

Methods

minBound :: StatIndex

maxBound :: StatIndex

Enum StatIndex

Methods

succ :: StatIndex -> StatIndex

pred :: StatIndex -> StatIndex

toEnum :: Int -> StatIndex

fromEnum :: StatIndex -> Int

enumFrom :: StatIndex -> [StatIndex]

enumFromThen :: StatIndex -> StatIndex -> [StatIndex]

enumFromTo :: StatIndex -> StatIndex -> [StatIndex]

enumFromThenTo :: StatIndex -> StatIndex -> StatIndex -> [StatIndex]

Eq StatIndex

Methods

(==) :: StatIndex -> StatIndex -> Bool

(/=) :: StatIndex -> StatIndex -> Bool

Ord StatIndex

Methods

compare :: StatIndex -> StatIndex -> Ordering

(<) :: StatIndex -> StatIndex -> Bool

(<=) :: StatIndex -> StatIndex -> Bool

(>) :: StatIndex -> StatIndex -> Bool

(>=) :: StatIndex -> StatIndex -> Bool

max :: StatIndex -> StatIndex -> StatIndex

min :: StatIndex -> StatIndex -> StatIndex

Read StatIndex

Methods

readsPrec :: Int -> ReadS StatIndex

readList :: ReadS [StatIndex]

readPrec :: ReadPrec StatIndex

readListPrec :: ReadPrec [StatIndex]

Show StatIndex

Methods

showsPrec :: Int -> StatIndex -> ShowS

show :: StatIndex -> String

showList :: [StatIndex] -> ShowS

incrementStat :: Solver -> StatIndex -> Int -> IO ()

increments a stat data corresponding to StatIndex

getStats :: Solver -> IO [(StatIndex, Int)]

returns the statistics as list