mios-1.2.1: A Minisat-based SAT solver in Haskell
SAT.Solver.Mios.Glucose
Description
This is a part of MIOS
Synopsis
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
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
>>>
nextReduction 0
nextReduction 1
nextReduction 2
nextReduction 3