toysolver-0.2.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Safe HaskellSafe-Inferred
LanguageHaskell2010

ToySolver.SAT.Types

Contents

Synopsis

Variable

type Var = Int Source

Variable is represented as positive integers (DIMACS format).

Model

class IModel a where Source

Methods

evalVar :: a -> Var -> Bool Source

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).

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.

Cardinality Constraint

type AtLeast = ([Lit], Int) Source

Pseudo Boolean Constraint

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.

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