SAT.Mios.Criteria

(This is a part of MIOS.) Advanced heuristics library for Main

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)

Clause

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.

Literal Block Distance

lbdOf :: Solver -> Stack -> IO Int

returns a POSIVITE value

Restart

checkRestartCondition :: Solver -> Int -> IO Bool

#62