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

Safe HaskellSafe
LanguageHaskell2010

SAT.Mios.Criteria

Contents

Description

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

Synopsis

Activities

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

Fig. 14 (p.19)

claDecayActivity :: Solver -> IO () Source #

Fig. 14 (p.19)

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

Fig. 14 (p.19) Bumping of clause activity

varDecayActivity :: Solver -> IO () Source #

Fig. 14 (p.19)

Clause

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).

Clause Metrics

lbdOf :: Solver -> Stack -> IO Int Source #

returns a POSIVITE value of Literal Block Distance

updateNDD :: Solver -> IO () Source #

updates all assigned vars' ndl

nddOf :: Solver -> Stack -> IO Int Source #

returns the NDL

Restart

Reporting

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

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