| Portability | non-portable (BangPatterns, DoRec, ScopedTypeVariables, CPP, DeriveDataTypeable) |
|---|---|
| Stability | provisional |
| Maintainer | masahiro.sakai@gmail.com |
| Safe Haskell | None |
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 ()
- 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 ()
- solve :: Solver -> IO Bool
- solveWith :: Solver -> [Lit] -> IO Bool
- data BudgetExceeded = BudgetExceeded
- type Model = UArray Var Bool
- model :: Solver -> IO Model
- failedAssumptions :: 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
- setVarPolarity :: Solver -> Var -> Bool -> IO ()
- setLogger :: Solver -> (String -> IO ()) -> IO ()
- setCheckModel :: Solver -> Bool -> IO ()
- setRandomFreq :: Solver -> Double -> IO ()
- defaultRandomFreq :: Double
- setRandomSeed :: Solver -> Int -> IO ()
- setConfBudget :: Solver -> Maybe Int -> IO ()
- nVars :: Solver -> IO Int
- nAssigns :: Solver -> IO Int
- nClauses :: Solver -> IO Int
- nLearnt :: Solver -> IO Int
- 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 -> BoolSource
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 >> return () = newVars_ solver n
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.
Solving
data BudgetExceeded Source
Constructors
| BudgetExceeded |
Extract results
failedAssumptions :: 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 :: RestartStrategySource
default value for RestartStrategy.
setRestartFirst :: Solver -> Int -> IO ()Source
The initial restart limit. (default 100) Negative value is used to disable restart.
defaultRestartFirst :: IntSource
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 :: DoubleSource
default value for RestartInc.
setLearntSizeFirst :: Solver -> Int -> IO ()Source
The initial limit for learnt clauses.
defaultLearntSizeFirst :: IntSource
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 :: DoubleSource
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
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
setRandomSeed :: Solver -> Int -> IO ()Source
Used by the random variable selection
Read state
Internal API
varBumpActivity :: Solver -> Var -> IO ()Source
varDecayActivity :: Solver -> IO ()Source