Safe Haskell	Safe-Inferred

SAT.Types

Contents

Variable
Model
Literal
Clause
Cardinality Constraint
Pseudo Boolean Constraint

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

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 :: Model -> 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.

Cardinality Constraint

normalizeAtLeast :: ([Lit], Int) -> ([Lit], Int)Source

Pseudo Boolean Constraint

normalizePBSum :: ([(Integer, Lit)], Integer) -> ([(Integer, Lit)], 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.

normalizePBAtLeast :: ([(Integer, Lit)], Integer) -> ([(Integer, Lit)], Integer)Source

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

normalizePBExactly :: ([(Integer, Lit)], Integer) -> ([(Integer, Lit)], Integer)Source

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

cutResolve :: ([(Integer, Lit)], Integer) -> ([(Integer, Lit)], Integer) -> Var -> ([(Integer, Lit)], Integer)Source

cardinalityReduction :: ([(Integer, Lit)], Integer) -> ([Lit], Int)Source

negatePBAtLeast :: ([(Integer, Lit)], Integer) -> ([(Integer, Lit)], Integer)Source

pbEval :: Model -> [(Integer, Lit)] -> Integer Source

pbLowerBound :: [(Integer, Lit)] -> Integer Source

pbUpperBound :: [(Integer, Lit)] -> Integer Source