ersatz-0.1: A monad for expressing SAT or QSAT problems using observable sharing.

Portability non-portable experimental Edward Kmett None

Ersatz.Internal.Formula

Contents

Description

Synopsis

Clauses

newtype Clause Source

A disjunction of possibly negated atoms. Negated atoms are represented by negating the identifier.

Constructors

 Clause FieldsclauseSet :: IntSet

Instances

 Eq Clause Ord Clause Show Clause Typeable Clause Monoid Clause QDIMACS Clause

Extract the (possibly negated) atoms referenced by a `Clause`.

Formulas

newtype Formula Source

A conjunction of clauses

Constructors

 Formula FieldsformulaSet :: Set Clause

Instances

 Eq Formula Ord Formula Show Formula Typeable Formula Monoid Formula QDIMACS Formula

A formula with no clauses

Assert a literal

Arguments

 :: Literal Output -> Literal Input -> Formula

The boolean not operation

``` O ≡ ¬A
(O → ¬A) & (¬O → A)
(¬O | ¬A) & (O | A)
```

Arguments

 :: Literal Output -> [Literal] Inputs -> Formula

The boolean and operation

``` O ≡ (A & B & C)
(O → (A & B & C)) & (¬O → ¬(A & B & C))
(¬O | (A & B & C)) & (O | ¬(A & B & C))
(¬O | A) & (¬O | B) & (¬O | C) & (O | ¬A | ¬B | ¬C)
```

Arguments

 :: Literal Output -> [Literal] Inputs -> Formula

The boolean or operation

``` O ≡ (A | B | C)
(O → (A | B | C)) & (¬O → ¬(A | B | C))
(¬O | (A | B | C)) & (O | ¬(A | B | C))
(¬O | A | B | C) & (O | (¬A & ¬B & ¬C))
(¬O | A | B | C) & (O | ¬A) & (O | ¬B) & (O | ¬C)
```

Arguments

 :: Literal Output -> Literal Input -> Literal Input -> Formula

The boolean xor operation

``` O ≡ A ⊕ B
O ≡ ((¬A & B) | (A & ¬B))
(O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))
```

Left hand side: ``` O → ((¬A & B) | (A & ¬B)) ¬O | ((¬A & B) | (A & ¬B)) ¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B)) ¬O | ((¬A | ¬B) & (A | B)) (¬O | ¬A | ¬B) & (¬O | A | B) ```

Right hand side:

``` ¬O → ¬((¬A & B) | (A & ¬B))
O | ¬((¬A & B) | (A & ¬B))
O | (¬(¬A & B) & ¬(A & ¬B))
O | ((A | ¬B) & (¬A | B))
(O | ¬A | B) & (O | A | ¬B)
```

Result:

``` (¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)
```

Arguments

 :: Literal Output -> Literal False branch -> Literal True branch -> Literal Predicate/selector -> Formula

The boolean else-then-if or mux operation

``` O ≡ (F & ¬P) | (T & P)
(O → ((F & ¬P) | (T & P))) & (¬O → ¬((F & ¬P) | (T & P)))
```

Left hand side:

``` O → ((F & ¬P) | (T & P))
¬O | ((F & ¬P) | (T & P))
¬O | ((F | T) & (F | P) & (T | ¬P) & (¬P | P))
¬O | ((F | T) & (F | P) & (T | ¬P))
(¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P)
```

Right hand side:

``` ¬O → ¬((F & ¬P) | (T & P))
O | ¬((F & ¬P) | (T & P))
O | (¬(F & ¬P) & ¬(T & P))
O | ((¬F | P) & (¬T | ¬P))
(O | ¬F | P) & (O | ¬T | ¬P)
```

Result:

``` (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P) & (O | ¬F | P) & (O | ¬T | ¬P)
```