SAT.Solver.Mios.M114

This is a part of MIOS

Documentation

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 Bool

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.