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

SAT.Types

Synopsis

# Variable

type Var = IntSource

Variable is represented as positive integers (DIMACS format).

# Model

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

# Literal

type Lit = IntSource

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

Arguments

 :: Var variable -> Bool polarity -> Lit

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

Negation of the `Lit`.

Underlying variable of the `Lit`

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

# Clause

type Clause = [Lit]Source

Disjunction of `Lit`.

Normalizing clause

`Nothing` if the clause is trivially true.

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