mios-1.2.1: A Minisat-based SAT solver in Haskell

Safe HaskellSafe
LanguageHaskell2010

SAT.Solver.Mios.Glucose

Description

This is a part of MIOS

Synopsis

Documentation

computeLBD :: Solver -> Vec -> IO Int Source #

returns the LBD vaule for 'Vec[1 ..]'

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

returns the LBD value of Clause

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

update the LBD field in Clause

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

update the lbd field of c

nextReduction :: Int -> Int -> Int Source #

0 based

>>> nextReduction 0
20000
>>> nextReduction 1
40000 + 200 = 20000 + 20000 + 200
>>> nextReduction 2
6000 + 600 = 20000 + 20200 + 20000 + 400
>>> nextReduction 3
80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600