SAT.Mios.Solver

This is a part of MIOS; main data

Solver

data Solver

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

Constructors

Solver

Fields

• model :: !(Vec Int)

  If found, this vector has the model

• conflicts :: !Stack

  Set of literals in the case of conflicts

• clauses :: !ClauseExtManager

  List of problem constraints.

• learnts :: !ClauseExtManager

  List of learnt clauses.

• watches :: !WatcherList

  list of constraint wathing p, literal-indexed

• assigns :: !(Vec Int)

  The current assignments indexed on variables

• phases :: !(Vec Int)

  The last assignments indexed on variables

• trail :: !Stack

  List of assignments in chronological order

• trailLim :: !Stack

  Separator indices for different decision levels in trail.

• qHead :: !Int'

  trail is divided at qHead; assignment part and queue part

• reason :: !ClauseVector

  For each variable, the constraint that implied its value

• level :: !(Vec Int)

  For each variable, the decision level it was assigned

• activities :: !(Vec Double)

  Heuristic measurement of the activity of a variable

• order :: !VarHeap

  Keeps track of the dynamic variable order.

• config :: !MiosConfiguration

  search paramerters

• nVars :: !Int

  number of variables

• varInc :: !Double'

  Variable activity increment amount to bump with.

• rootLevel :: !Int'

  Separates incremental and search assumptions.

• ok :: !Bool'

  return value holder

• an'seen :: !(Vec Int)

  used in analyze

• an'toClear :: !Stack

  used in analyze

• an'stack :: !Stack

  used in analyze

• an'lastDL :: !Stack

  last decision level used in analyze

• litsLearnt :: !Stack

  used in analyze and search to create a learnt clause

• stats :: !(UVector Int)

  statistics information holder

Instances

VarOrder Solver

Interfate to select a decision var based on variable activity.

Methods

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

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

select :: Solver -> IO Var

data VarHeap

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.

newSolver :: MiosConfiguration -> CNFDescription -> IO Solver

returns an everything-is-initialized solver from the arguments.

getModel :: Solver -> IO [Int]

returns the model as a list of literal.

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

State Modifiers

addClause :: Solver -> Stack -> 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).

Activities

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

Fig. 14 (p.19)

claRescaleActivityAfterRestart :: 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)

claActivityThreshold :: Double

value for rescaling clause activity.

Stats

data StatIndex

stat index

Constructors

NumOfBackjump

the number of backjump

NumOfRestart

the number of restart

EndOfStatIndex

Don't use this dummy.

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

getStat :: Solver -> StatIndex -> IO Int

returns the value of StatIndex.

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

sets to StatIndex.

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

increments a stat data corresponding to StatIndex.

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

returns the statistics as a list.