mios-1.6.2: A Minisat-based CDCL SAT solver in Haskell

Safe HaskellSafe




(This is a part of MIOS.) Main part of solving satisfiability problem.


Interface to Solver, imported from Criteria

data Solver Source #

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

VarOrder Solver Source #

Interfate to select a decision var based on variable activity.

Instance details

Defined in SAT.Mios.Solver


updateVO :: Solver -> Var -> IO () Source #

undoVO :: Solver -> Var -> IO () Source #

selectVO :: Solver -> IO Var Source #

newSolver :: MiosConfiguration -> CNFDescription -> IO Solver Source #

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

setAssign :: Solver -> Int -> LiftedBool -> IO () Source #

assigns a value to the n-th variable

addClause :: Solver -> Stack -> IO Bool Source #

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

dumpStats :: DumpMode -> Solver -> IO () Source #

print statatistic data to stdio. This should be called after each restart.

Main function

simplifyDB :: Solver -> IO Bool Source #


simplify : [void] -> [bool]

Description: Simplify the clause database according to the current top-level assigment. Currently, the only thing done here is the removal of satisfied clauses, but more things can be put here.

solve :: Foldable t => Solver -> t Lit -> IO SolverResult Source #

Fig. 16. (p.20) Main solve method.

Pre-condition: If assumptions are used, simplifyDB must be called right before using this method. If not, a top-level conflict (resulting in a non-usable internal state) cannot be distinguished from a conflict under assumptions.