Safe Haskell	Safe-Inferred
Language	Haskell2010

ToySolver.SAT.Types

Contents

Variable
Model
Literal
Clause
Cardinality Constraint
Pseudo Boolean Constraint
XOR Clause

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

Methods

evalVar :: a -> Var -> Bool Source

Instances

IModel (Var -> Bool)
IModel (UArray Var Bool)
IModel (Array Var Bool)

type Model = UArray Var Bool Source

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

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

normalizeAtLeast :: AtLeast -> AtLeast Source

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

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

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

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