| 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:
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 Lit
- 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
- 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 [Lit]
- getAssumptionsImplications :: Solver -> IO [Lit]
- module ToySolver.SAT.Config
- getConfig :: Solver -> IO Config
- setConfig :: Solver -> Config -> IO ()
- modifyConfig :: Solver -> (Config -> Config) -> IO ()
- setVarPolarity :: Solver -> Var -> Bool -> IO ()
- setLogger :: Solver -> (String -> IO ()) -> IO ()
- setRandomGen :: Solver -> GenIO -> IO ()
- getRandomGen :: Solver -> IO GenIO
- setConfBudget :: Solver -> Maybe Int -> 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
| AddXORClause IO Solver Source # | |
| AddPBLin IO Solver Source # | |
Defined in ToySolver.SAT 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 # | |
| AddCardinality IO Solver Source # | |
| AddClause 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 # | |
| PrimMonad m => AddClause m (PBStore 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 # | |
type PackedClause = Vector Lit 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 (PBStore m) Source # | |
| Monad m => AddCardinality m (Encoder m) Source # | |
| PrimMonad m => AddCardinality m (Encoder m) Source # | |
| PrimMonad m => AddCardinality m (Encoder 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)
Theory
Solving
data BudgetExceeded Source #
Constructors
| BudgetExceeded |
Instances
| Show BudgetExceeded Source # | |
Defined in ToySolver.SAT Methods showsPrec :: Int -> BudgetExceeded -> ShowS # show :: BudgetExceeded -> String # showList :: [BudgetExceeded] -> ShowS # | |
| Exception BudgetExceeded Source # | |
Defined in ToySolver.SAT Methods toException :: BudgetExceeded -> SomeException # | |
Constructors
| Canceled |
Instances
| Show Canceled Source # | |
| Exception Canceled Source # | |
Defined in ToySolver.SAT Methods toException :: Canceled -> SomeException # fromException :: SomeException -> Maybe Canceled # displayException :: Canceled -> String # | |
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 [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.
getAssumptionsImplications :: Solver -> IO [Lit] 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
module ToySolver.SAT.Config
setLogger :: Solver -> (String -> IO ()) -> IO () Source #
set callback function for receiving messages.
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
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 #