| Copyright | (c) Masahiro Sakai 2012-2014 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable (BangPatterns, ScopedTypeVariables, CPP, DeriveDataTypeable, RecursiveDo) |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT
Contents
Description
A CDCL SAT solver.
It follows the design of MiniSat and SAT4J.
See also:
- data Solver
- newSolver :: IO Solver
- type Var = Int
- type Lit = Int
- literal :: Var -> Bool -> Lit
- litNot :: Lit -> Lit
- litVar :: Lit -> Var
- litPolarity :: Lit -> Bool
- type Clause = [Lit]
- newVar :: Solver -> IO Var
- newVars :: Solver -> Int -> IO [Var]
- newVars_ :: Solver -> Int -> IO ()
- resizeVarCapacity :: Solver -> Int -> IO ()
- addClause :: Solver -> Clause -> IO ()
- addAtLeast :: Solver -> [Lit] -> Int -> IO ()
- addAtMost :: Solver -> [Lit] -> Int -> IO ()
- addExactly :: Solver -> [Lit] -> Int -> IO ()
- addPBAtLeast :: Solver -> [(Integer, Lit)] -> Integer -> IO ()
- addPBAtMost :: Solver -> [(Integer, Lit)] -> Integer -> IO ()
- addPBExactly :: Solver -> [(Integer, Lit)] -> Integer -> IO ()
- addPBAtLeastSoft :: Solver -> Lit -> [(Integer, Lit)] -> Integer -> IO ()
- addPBAtMostSoft :: Solver -> Lit -> [(Integer, Lit)] -> Integer -> IO ()
- addPBExactlySoft :: Solver -> Lit -> [(Integer, Lit)] -> Integer -> IO ()
- addXORClause :: Solver -> [Lit] -> Bool -> IO ()
- addXORClauseSoft :: Solver -> Lit -> [Lit] -> Bool -> IO ()
- solve :: Solver -> IO Bool
- solveWith :: Solver -> [Lit] -> IO Bool
- data BudgetExceeded = BudgetExceeded
- type Model = UArray Var Bool
- getModel :: Solver -> IO Model
- getFailedAssumptions :: Solver -> IO [Lit]
- data RestartStrategy
- setRestartStrategy :: Solver -> RestartStrategy -> IO ()
- defaultRestartStrategy :: RestartStrategy
- setRestartFirst :: Solver -> Int -> IO ()
- defaultRestartFirst :: Int
- setRestartInc :: Solver -> Double -> IO ()
- defaultRestartInc :: Double
- setLearntSizeFirst :: Solver -> Int -> IO ()
- defaultLearntSizeFirst :: Int
- setLearntSizeInc :: Solver -> Double -> IO ()
- defaultLearntSizeInc :: Double
- setCCMin :: Solver -> Int -> IO ()
- defaultCCMin :: Int
- data LearningStrategy
- setLearningStrategy :: Solver -> LearningStrategy -> IO ()
- defaultLearningStrategy :: LearningStrategy
- setEnablePhaseSaving :: Solver -> Bool -> IO ()
- getEnablePhaseSaving :: Solver -> IO Bool
- defaultEnablePhaseSaving :: Bool
- setEnableForwardSubsumptionRemoval :: Solver -> Bool -> IO ()
- getEnableForwardSubsumptionRemoval :: Solver -> IO Bool
- defaultEnableForwardSubsumptionRemoval :: Bool
- setEnableBackwardSubsumptionRemoval :: Solver -> Bool -> IO ()
- getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool
- defaultEnableBackwardSubsumptionRemoval :: Bool
- setVarPolarity :: Solver -> Var -> Bool -> IO ()
- setLogger :: Solver -> (String -> IO ()) -> IO ()
- setCheckModel :: Solver -> Bool -> IO ()
- setRandomFreq :: Solver -> Double -> IO ()
- defaultRandomFreq :: Double
- setRandomGen :: Solver -> StdGen -> IO ()
- getRandomGen :: Solver -> IO StdGen
- setConfBudget :: Solver -> Maybe Int -> IO ()
- data PBHandlerType
- setPBHandlerType :: Solver -> PBHandlerType -> IO ()
- defaultPBHandlerType :: PBHandlerType
- nVars :: Solver -> IO Int
- nAssigns :: Solver -> IO Int
- nConstraints :: Solver -> IO Int
- nLearnt :: Solver -> IO Int
- getVarFixed :: Solver -> Var -> IO LBool
- getLitFixed :: Solver -> Var -> IO LBool
- varBumpActivity :: Solver -> Var -> IO ()
- varDecayActivity :: Solver -> IO ()
The Solver type
Basic data structures
Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).
litPolarity :: Lit -> Bool Source
Problem specification
newVars :: Solver -> Int -> IO [Var] Source
Add variables. newVars solver n = replicateM n (newVar solver)
newVars_ :: Solver -> Int -> IO () Source
Add variables. newVars_ solver n = newVars solver n >> return ()
resizeVarCapacity :: Solver -> Int -> IO () Source
Pre-allocate internal buffer for n variables.
Arguments
| :: Solver | The |
| -> [Lit] | set of literals {l1,l2,..} (duplicated elements are ignored) |
| -> Int | n. |
| -> IO () |
Add a cardinality constraints atleast({l1,l2,..},n).
Arguments
| :: Solver | The |
| -> [Lit] | set of literals {l1,l2,..} (duplicated elements are ignored) |
| -> Int | n |
| -> IO () |
Add a cardinality constraints atmost({l1,l2,..},n).
Arguments
| :: Solver | The |
| -> [Lit] | set of literals {l1,l2,..} (duplicated elements are ignored) |
| -> Int | n |
| -> IO () |
Add a cardinality constraints exactly({l1,l2,..},n).
Arguments
| :: Solver | The |
| -> [(Integer, Lit)] | set of terms |
| -> Integer | n |
| -> IO () |
Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≥ n.
Arguments
| :: Solver | The |
| -> [(Integer, Lit)] | list of |
| -> Integer | n |
| -> IO () |
Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≤ n.
Arguments
| :: Solver | The |
| -> [(Integer, Lit)] | list of terms |
| -> Integer | n |
| -> IO () |
Add a pseudo boolean constraints c1*l1 + c2*l2 + … = n.
Arguments
| :: Solver | The |
| -> Lit | indicator |
| -> [(Integer, Lit)] | set of terms |
| -> Integer | n |
| -> IO () |
Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … ≥ n.
Arguments
| :: Solver | The |
| -> Lit | indicator |
| -> [(Integer, Lit)] | set of terms |
| -> Integer | n |
| -> IO () |
Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … ≤ n.
Arguments
| :: Solver | The |
| -> Lit | indicator |
| -> [(Integer, Lit)] | set of terms |
| -> Integer | n |
| -> IO () |
Add a soft pseudo boolean constraints lit ⇒ c1*l1 + c2*l2 + … = n.
Add a parity constraint l1 ⊕ l2 ⊕ … ⊕ ln = rhs
Arguments
| :: Solver | The |
| -> Lit | indicator |
| -> [Lit] | literals |
| -> Bool | rhs |
| -> IO () |
Add a soft parity constraint lit ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs
Solving
Extract results
type Model = UArray Var Bool Source
A model is represented as a mapping from variables to its values.
getFailedAssumptions :: Solver -> IO [Lit] Source
After solveWith returns False, it returns a set of assumptions
that leads to contradiction. In particular, if it returns an empty
set, the problem is unsatisiable without any assumptions.
Solver configulation
setRestartStrategy :: Solver -> RestartStrategy -> IO () Source
defaultRestartStrategy :: RestartStrategy Source
default value for RestartStrategy.
setRestartFirst :: Solver -> Int -> IO () Source
The initial restart limit. (default 100) Negative value is used to disable restart.
defaultRestartFirst :: Int Source
default value for RestartFirst.
setRestartInc :: Solver -> Double -> IO () Source
The factor with which the restart limit is multiplied in each restart. (default 1.5)
defaultRestartInc :: Double Source
default value for RestartInc.
setLearntSizeFirst :: Solver -> Int -> IO () Source
The initial limit for learnt clauses.
defaultLearntSizeFirst :: Int Source
default value for LearntSizeFirst.
setLearntSizeInc :: Solver -> Double -> IO () Source
The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
defaultLearntSizeInc :: Double Source
default value for LearntSizeInc.
setCCMin :: Solver -> Int -> IO () Source
The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
default value for CCMin.
data LearningStrategy Source
Constructors
| LearningClause | |
| LearningHybrid |
setLearningStrategy :: Solver -> LearningStrategy -> IO () Source
setEnablePhaseSaving :: Solver -> Bool -> IO () Source
getEnablePhaseSaving :: Solver -> IO Bool Source
setEnableForwardSubsumptionRemoval :: Solver -> Bool -> IO () Source
setEnableBackwardSubsumptionRemoval :: Solver -> Bool -> IO () Source
setLogger :: Solver -> (String -> IO ()) -> IO () Source
set callback function for receiving messages.
setCheckModel :: Solver -> Bool -> IO () Source
setRandomFreq :: Solver -> Double -> IO () Source
The frequency with which the decision heuristic tries to choose a random variable
setRandomGen :: Solver -> StdGen -> IO () Source
Set random generator used by the random variable selection
getRandomGen :: Solver -> IO StdGen Source
Get random generator used by the random variable selection
setPBHandlerType :: Solver -> PBHandlerType -> IO () Source
Read state
nConstraints :: Solver -> IO Int Source
number of constraints.
Internal API
varBumpActivity :: Solver -> Var -> IO () Source
varDecayActivity :: Solver -> IO () Source