SAT.Mios.Main

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

Interface to Solver, imported from Criteria

data Solver

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

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

newSolver :: MiosConfiguration -> CNFDescription -> IO Solver

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

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

assigns a value to the n-th variable

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.

dumpSolver :: DumpMode -> Solver -> IO ()

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

Main function

simplifyDB :: Solver -> IO Bool

#M22

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

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.