| Copyright | (c) Masahiro Sakai 2012-2014 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
| Extensions |
|
ToySolver.SAT.Solver.CDCL
Description
A CDCL SAT solver.
It follows the design of MiniSat and SAT4J.
See also:
Synopsis
- data Solver
- newSolver :: IO Solver
- newSolverWithConfig :: Config -> IO Solver
- type Var = Int
- type Lit = Int
- literal :: Var -> Bool -> Lit
- litNot :: Lit -> Lit
- litVar :: Lit -> Var
- litPolarity :: Lit -> Bool
- evalLit :: IModel m => m -> Lit -> Bool
- newVar :: NewVar m a => a -> m Var
- newVars :: NewVar m a => a -> Int -> m [Var]
- newVars_ :: NewVar m a => a -> Int -> m ()
- resizeVarCapacity :: Solver -> Int -> IO ()
- class NewVar m a => AddClause m a | a -> m where
- type Clause = [Lit]
- evalClause :: IModel m => m -> Clause -> Bool
- type PackedClause = Vector PackedLit
- packClause :: Clause -> PackedClause
- unpackClause :: PackedClause -> Clause
- class AddClause m a => AddCardinality m a | a -> m where
- addAtLeast :: a -> [Lit] -> Int -> m ()
- addAtMost :: a -> [Lit] -> Int -> m ()
- addExactly :: a -> [Lit] -> Int -> m ()
- type AtLeast = ([Lit], Int)
- type Exactly = ([Lit], Int)
- evalAtLeast :: IModel m => m -> AtLeast -> Bool
- evalExactly :: IModel m => m -> Exactly -> Bool
- class AddCardinality m a => AddPBLin m a | a -> m where
- addPBAtLeast :: a -> PBLinSum -> Integer -> m ()
- addPBAtMost :: a -> PBLinSum -> Integer -> m ()
- addPBExactly :: a -> PBLinSum -> Integer -> m ()
- addPBAtLeastSoft :: a -> Lit -> PBLinSum -> Integer -> m ()
- addPBAtMostSoft :: a -> Lit -> PBLinSum -> Integer -> m ()
- addPBExactlySoft :: a -> Lit -> PBLinSum -> Integer -> m ()
- type PBLinTerm = (Integer, Lit)
- type PBLinSum = [PBLinTerm]
- type PBLinAtLeast = (PBLinSum, Integer)
- type PBLinExactly = (PBLinSum, Integer)
- evalPBLinSum :: IModel m => m -> PBLinSum -> Integer
- evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
- evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool
- class AddClause m a => AddXORClause m a | a -> m where
- addXORClause :: a -> [Lit] -> Bool -> m ()
- addXORClauseSoft :: a -> Lit -> [Lit] -> Bool -> m ()
- type XORClause = ([Lit], Bool)
- evalXORClause :: IModel m => m -> XORClause -> Bool
- addSOS2 :: AddClause m a => a -> [Lit] -> m ()
- evalSOS2 :: IModel m => m -> [Lit] -> Bool
- setTheory :: Solver -> TheorySolver -> IO ()
- solve :: Solver -> IO Bool
- solveWith :: Solver -> [Lit] -> IO Bool
- data BudgetExceeded = BudgetExceeded
- cancel :: Solver -> IO ()
- data Canceled = Canceled
- class IModel a where
- type Model = UArray Var Bool
- getModel :: Solver -> IO Model
- getFailedAssumptions :: Solver -> IO LitSet
- getAssumptionsImplications :: Solver -> IO LitSet
- module ToySolver.SAT.Solver.CDCL.Config
- getConfig :: Solver -> IO Config
- setConfig :: Solver -> Config -> IO ()
- modifyConfig :: Solver -> (Config -> Config) -> IO ()
- setVarPolarity :: Solver -> Var -> Bool -> IO ()
- setRandomGen :: Solver -> GenIO -> IO ()
- getRandomGen :: Solver -> IO GenIO
- setConfBudget :: Solver -> Maybe Int -> IO ()
- setLogger :: Solver -> (String -> IO ()) -> IO ()
- clearLogger :: Solver -> IO ()
- setTerminateCallback :: Solver -> IO Bool -> IO ()
- clearTerminateCallback :: Solver -> IO ()
- setLearnCallback :: Solver -> (Clause -> IO ()) -> IO ()
- clearLearnCallback :: Solver -> IO ()
- getNVars :: Solver -> IO Int
- getNConstraints :: Solver -> IO Int
- getNLearntConstraints :: Solver -> IO Int
- getVarFixed :: Solver -> Var -> IO LBool
- getLitFixed :: Solver -> Lit -> IO LBool
- getFixedLiterals :: Solver -> IO [Lit]
- varBumpActivity :: Solver -> Var -> IO ()
- varDecayActivity :: Solver -> IO ()
The Solver type
Solver instance
Instances
| AddCardinality IO Solver Source # | |
| AddClause IO Solver Source # | |
| AddPBLin IO Solver Source # | |
Defined in ToySolver.SAT.Solver.CDCL Methods addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO () Source # addPBAtMost :: Solver -> PBLinSum -> Integer -> IO () Source # addPBExactly :: Solver -> PBLinSum -> Integer -> IO () Source # addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source # addPBAtMostSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source # addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO () Source # | |
| AddXORClause IO Solver Source # | |
| NewVar IO Solver Source # | |
newSolverWithConfig :: Config -> IO Solver Source #
Create a new Solver instance with a given configulation.
Basic data structures
Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).
litPolarity :: Lit -> Bool Source #
Problem specification
newVars :: NewVar m a => a -> Int -> m [Var] Source #
Add variables. newVars a n = replicateM n (newVar a), but maybe faster.
newVars_ :: NewVar m a => a -> Int -> m () Source #
Add variables. newVars_ a n = newVars a n >> return (), but maybe faster.
Clauses
class NewVar m a => AddClause m a | a -> m where Source #
Instances
| AddClause IO Solver Source # | |
| Monad m => AddClause m (Encoder m) Source # | |
| Monad m => AddClause m (Encoder m) Source # | |
| Monad m => AddClause m (Encoder m) Source # | |
| Monad m => AddClause m (Encoder m) Source # | |
| Monad m => AddClause m (Encoder m) Source # | |
| PrimMonad m => AddClause m (CNFStore m) Source # | |
| PrimMonad m => AddClause m (PBStore m) Source # | |
type PackedClause = Vector PackedLit Source #
packClause :: Clause -> PackedClause Source #
unpackClause :: PackedClause -> Clause Source #
Cardinality constraints
class AddClause m a => AddCardinality m a | a -> m where Source #
Minimal complete definition
Methods
Add a cardinality constraints atleast({l1,l2,..},n).
Add a cardinality constraints atmost({l1,l2,..},n).
Add a cardinality constraints exactly({l1,l2,..},n).
Instances
| AddCardinality IO Solver Source # | |
| PrimMonad m => AddCardinality m (Encoder m) Source # | |
| PrimMonad m => AddCardinality m (Encoder m) Source # | |
| Monad m => AddCardinality m (Encoder m) Source # | |
| PrimMonad m => AddCardinality m (PBStore m) Source # | |
(Linear) pseudo-boolean constraints
class AddCardinality m a => AddPBLin m a | a -> m where Source #
Minimal complete definition
Methods
Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≥ n.
Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≤ n.
Add a pseudo boolean constraints c1*l1 + c2*l2 + … = n.
Arguments
| :: a | |
| -> Lit | Selector literal |
| -> PBLinSum | list of terms |
| -> Integer | n |
| -> m () |
Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≥ n.
Arguments
| :: a | |
| -> Lit | Selector literal |
| -> PBLinSum | list of terms |
| -> Integer | n |
| -> m () |
Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≤ n.
Arguments
| :: a | |
| -> Lit | Selector literal |
| -> PBLinSum | list of terms |
| -> Integer | n |
| -> m () |
Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … = n.
Instances
type PBLinAtLeast = (PBLinSum, Integer) Source #
type PBLinExactly = (PBLinSum, Integer) Source #
evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool Source #
evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool Source #
XOR clauses
class AddClause m a => AddXORClause m a | a -> m where Source #
Minimal complete definition
Methods
Add a parity constraint l1 ⊕ l2 ⊕ … ⊕ ln = rhs
Add a soft parity constraint sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs
type XORClause = ([Lit], Bool) Source #
XOR clause
'([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.
Note that:
- True can be represented as ([], False)
- False can be represented as ([], True)
Type-2 SOS constraints
addSOS2 :: AddClause m a => a -> [Lit] -> m () Source #
Add a type-2 SOS constraint
At most two adjacnt literals can be true.
Theory
Solving
data BudgetExceeded Source #
Constructors
| BudgetExceeded |
Instances
| Exception BudgetExceeded Source # | |
Defined in ToySolver.SAT.Solver.CDCL Methods toException :: BudgetExceeded -> SomeException # | |
| Show BudgetExceeded Source # | |
Defined in ToySolver.SAT.Solver.CDCL Methods showsPrec :: Int -> BudgetExceeded -> ShowS # show :: BudgetExceeded -> String # showList :: [BudgetExceeded] -> ShowS # | |
Constructors
| Canceled |
Instances
| Exception Canceled Source # | |
Defined in ToySolver.SAT.Solver.CDCL Methods toException :: Canceled -> SomeException # fromException :: SomeException -> Maybe Canceled # displayException :: Canceled -> String # | |
| Show Canceled Source # | |
Extract results
type Model = UArray Var Bool Source #
A model is represented as a mapping from variables to its values.
getModel :: Solver -> IO Model Source #
After solve returns True, it returns an satisfying assignment.
getFailedAssumptions :: Solver -> IO LitSet 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.
getAssumptionsImplications :: Solver -> IO LitSet Source #
EXPERIMENTAL API: After solveWith returns True or failed with BudgetExceeded exception,
it returns a set of literals that are implied by assumptions.
Solver configulation
setRandomGen :: Solver -> GenIO -> IO () Source #
Set random generator used by the random variable selection
getRandomGen :: Solver -> IO GenIO Source #
Get random generator used by the random variable selection
Callbacks
setLogger :: Solver -> (String -> IO ()) -> IO () Source #
set callback function for receiving messages.
setTerminateCallback :: Solver -> IO Bool -> IO () Source #
Set a callback function used to indicate a termination requirement to the solver.
The solver will periodically call this function and check its return value during
the search. If the callback function returns True the solver terminates and throws
Canceled exception.
See also clearTerminateCallback and
IPASIR's ipasir_set_terminate() function.
clearTerminateCallback :: Solver -> IO () Source #
Clear a callback function set by setTerminateCallback
setLearnCallback :: Solver -> (Clause -> IO ()) -> IO () Source #
Set a callback function used to extract learned clauses from the solver. The solver will call this function for each learned clause.
See also clearLearnCallback and
IPASIR's ipasir_set_learn() function.
clearLearnCallback :: Solver -> IO () Source #
Clear a callback function set by setLearnCallback
Read state
getFixedLiterals :: Solver -> IO [Lit] Source #
it returns a set of literals that are fixed without any assumptions.
Internal API
varDecayActivity :: Solver -> IO () Source #