Safe Haskell	None
Language	Haskell2010

ToySolver.SAT.Types

Contents

Variable
Model
Literal
Clause
Cardinality Constraint
(Linear) Pseudo Boolean Constraint
Non-linear Pseudo Boolean constraint
XOR Clause
Type classes for solvers

Synopsis

Variable

type Var = Int Source #

Variable is represented as positive integers (DIMACS format).

type VarSet = IntSet Source #

type VarMap = IntMap Source #

validVar :: Var -> Bool Source #

Model

class IModel a where Source #

Minimal complete definition

evalVar

Methods

evalVar :: a -> Var -> Bool Source #

Instances

IModel (Var -> Bool) Source #
Methods evalVar :: (Var -> Bool) -> Var -> Bool Source #
IModel (UArray Var Bool) Source #
Methods evalVar :: UArray Var Bool -> Var -> Bool Source #
IModel (Array Var Bool) Source #
Methods evalVar :: Array Var Bool -> Var -> Bool Source #

type Model = UArray Var Bool Source #

A model is represented as a mapping from variables to its values.

restrictModel :: Int -> Model -> Model Source #

Restrict model to first nv variables.

Literal

type Lit = Int Source #

Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).

type LitSet = IntSet Source #

type LitMap = IntMap Source #

litUndef :: Lit Source #

validLit :: Lit -> Bool Source #

literal Source #

Arguments

:: Var	variable
-> Bool	polarity
-> Lit

Construct a literal from a variable and its polarity. True (resp False) means positive (resp. negative) literal.

litNot :: Lit -> Lit Source #

Negation of the Lit.

litVar :: Lit -> Var Source #

Underlying variable of the Lit

litPolarity :: Lit -> Bool Source #

Polarity of the Lit. True means positive literal and False means negative literal.

evalLit :: IModel m => m -> Lit -> Bool Source #

Clause

type Clause = [Lit] Source #

Disjunction of Lit.

normalizeClause :: Clause -> Maybe Clause Source #

Normalizing clause

Nothing if the clause is trivially true.

instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause) Source #

clauseSubsume :: Clause -> Clause -> Bool Source #

evalClause :: IModel m => m -> Clause -> Bool Source #

clauseToPBLinAtLeast :: Clause -> PBLinAtLeast Source #

Cardinality Constraint

type AtLeast = ([Lit], Int) Source #

type Exactly = ([Lit], Int) Source #

normalizeAtLeast :: AtLeast -> AtLeast Source #

instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast Source #

evalAtLeast :: IModel m => m -> AtLeast -> Bool Source #

evalExactly :: IModel m => m -> Exactly -> Bool Source #

(Linear) Pseudo Boolean Constraint

type PBLinTerm = (Integer, Lit) Source #

type PBLinSum = [PBLinTerm] Source #

type PBLinAtLeast = (PBLinSum, Integer) Source #

type PBLinExactly = (PBLinSum, Integer) Source #

normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer) Source #

normalizing PB term of the form c1 x1 + c2 x2 ... cn xn + c into d1 x1 + d2 x2 ... dm xm + d where d1,...,dm ≥ 1.

normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast Source #

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn >= b.

normalizePBLinExactly :: PBLinExactly -> PBLinExactly Source #

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn = b.

instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast Source #

instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly Source #

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast Source #

cardinalityReduction :: PBLinAtLeast -> AtLeast Source #

negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast Source #

evalPBLinSum :: IModel m => m -> PBLinSum -> Integer Source #

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool Source #

evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool Source #

pbLowerBound :: PBLinSum -> Integer Source #

pbUpperBound :: PBLinSum -> Integer Source #

pbSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool Source #

evalPBConstraint :: IModel m => m -> Constraint -> Bool Source #

Non-linear Pseudo Boolean constraint

type PBTerm = (Integer, [Lit]) Source #

type PBSum = [PBTerm] Source #

evalPBSum :: IModel m => m -> PBSum -> Integer Source #

XOR Clause

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)

normalizeXORClause :: XORClause -> XORClause Source #

Normalize XOR clause

instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause Source #

evalXORClause :: IModel m => m -> XORClause -> Bool Source #

Type classes for solvers

class Monad m => NewVar m a | a -> m where Source #

Minimal complete definition

newVar

Methods

newVar :: a -> m Var Source #

Add a new variable

newVars :: a -> Int -> m [Var] Source #

Add variables. newVars a n = replicateM n (newVar a), but maybe faster.

newVars_ :: a -> Int -> m () Source #

Add variables. newVars_ a n = newVars a n >> return (), but maybe faster.

Instances

NewVar IO Solver Source #
Methods newVar :: Solver -> IO Var Source # newVars :: Solver -> Int -> IO [Var] Source # newVars_ :: Solver -> Int -> IO () Source #
Monad m => NewVar m (Encoder m) Source #
Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #
PrimMonad m => NewVar m (PBStore m) Source #
Methods newVar :: PBStore m -> m Var Source # newVars :: PBStore m -> Int -> m [Var] Source # newVars_ :: PBStore m -> Int -> m () Source #
PrimMonad m => NewVar m (CNFStore m) Source #
Methods newVar :: CNFStore m -> m Var Source # newVars :: CNFStore m -> Int -> m [Var] Source # newVars_ :: CNFStore m -> Int -> m () Source #

class NewVar m a => AddClause m a | a -> m where Source #

Minimal complete definition

addClause

Methods

addClause :: a -> Clause -> m () Source #

Instances

AddClause IO Solver Source #
Methods addClause :: Solver -> Clause -> IO () Source #
Monad m => AddClause m (Encoder m) Source #
Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Methods addClause :: Encoder m -> Clause -> m () Source #
PrimMonad m => AddClause m (PBStore m) Source #
Methods addClause :: PBStore m -> Clause -> m () Source #
PrimMonad m => AddClause m (CNFStore m) Source #
Methods addClause :: CNFStore m -> Clause -> m () Source #

class AddClause m a => AddCardinality m a | a -> m where Source #

Minimal complete definition

addAtLeast

Methods

addAtLeast :: a -> [Lit] -> Int -> m () Source #

Add a cardinality constraints atleast({l1,l2,..},n).

addAtMost :: a -> [Lit] -> Int -> m () Source #

Add a cardinality constraints atmost({l1,l2,..},n).

addExactly :: a -> [Lit] -> Int -> m () Source #

Add a cardinality constraints exactly({l1,l2,..},n).

Instances

AddCardinality IO Solver Source #
Methods addAtLeast :: Solver -> [Lit] -> Int -> IO () Source # addAtMost :: Solver -> [Lit] -> Int -> IO () Source # addExactly :: Solver -> [Lit] -> Int -> IO () Source #
PrimMonad m => AddCardinality m (Encoder m) Source #
Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
Monad m => AddCardinality m (Encoder m) Source #
Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
PrimMonad m => AddCardinality m (PBStore m) Source #
Methods addAtLeast :: PBStore m -> [Lit] -> Int -> m () Source # addAtMost :: PBStore m -> [Lit] -> Int -> m () Source # addExactly :: PBStore m -> [Lit] -> Int -> m () Source #

class AddCardinality m a => AddPBLin m a | a -> m where Source #

Minimal complete definition

addPBAtLeast

Methods

addPBAtLeast :: a -> PBLinSum -> Integer -> m () Source #

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≥ n.

addPBAtMost :: a -> PBLinSum -> Integer -> m () Source #

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≤ n.

addPBExactly :: a -> PBLinSum -> Integer -> m () Source #

Add a pseudo boolean constraints c1*l1 + c2*l2 + … = n.

addPBAtLeastSoft :: a -> Lit -> PBLinSum -> Integer -> m () Source #

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≥ n.

addPBAtMostSoft :: a -> Lit -> PBLinSum -> Integer -> m () Source #

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≤ n.

addPBExactlySoft :: a -> Lit -> PBLinSum -> Integer -> m () Source #

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … = n.

Instances

AddPBLin IO Solver Source #
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 #
PrimMonad m => AddPBLin m (Encoder m) Source #
Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
Monad m => AddPBLin m (Encoder m) Source #
Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
PrimMonad m => AddPBLin m (PBStore m) Source #
Methods addPBAtLeast :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBExactly :: PBStore m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m () Source #

class AddPBLin m a => AddPBNL m a | a -> m where Source #

Minimal complete definition

addPBNLAtLeast

Methods

addPBNLAtLeast :: a -> PBSum -> Integer -> m () Source #

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMost :: a -> PBSum -> Integer -> m () Source #

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLExactly :: a -> PBSum -> Integer -> m () Source #

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … = n.

addPBNLAtLeastSoft :: a -> Lit -> PBSum -> Integer -> m () Source #

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMostSoft :: a -> Lit -> PBSum -> Integer -> m () Source #

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≤ n.

addPBNLExactlySoft :: a -> Lit -> PBSum -> Integer -> m () Source #

Add a soft non-linear pseudo boolean constraints lit ⇒ c1*ls1 + c2*ls2 + … = n.

Instances

PrimMonad m => AddPBNL m (Encoder m) Source #
Methods addPBNLAtLeast :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtMost :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLExactly :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtLeastSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLAtMostSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLExactlySoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source #
PrimMonad m => AddPBNL m (PBStore m) Source #
Methods addPBNLAtLeast :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLAtMost :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLExactly :: PBStore m -> PBSum -> Integer -> m () Source # addPBNLAtLeastSoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source # addPBNLAtMostSoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source # addPBNLExactlySoft :: PBStore m -> Lit -> PBSum -> Integer -> m () Source #

class AddClause m a => AddXORClause m a | a -> m where Source #

Minimal complete definition

addXORClause

Methods

addXORClause :: a -> [Lit] -> Bool -> m () Source #

Add a parity constraint l1 ⊕ l2 ⊕ … ⊕ ln = rhs

addXORClauseSoft :: a -> Lit -> [Lit] -> Bool -> m () Source #

Add a soft parity constraint sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs

Instances

AddXORClause IO Solver Source #
Methods addXORClause :: Solver -> [Lit] -> Bool -> IO () Source # addXORClauseSoft :: Solver -> Lit -> [Lit] -> Bool -> IO () Source #