funsat-0.6.0: A modern DPLL-style SAT solver

Funsat.Circuit

Description

A circuit is a standard one of among many ways of representing a propositional logic formula. This module provides a flexible circuit type class and various representations that admit efficient conversion to funsat CNF.

Synopsis

## Circuit type class

class Circuit repr whereSource

A class representing a grammar for logical circuits. Default implemenations are indicated.

Methods

true :: (Ord var, Show var) => repr varSource

false :: (Ord var, Show var) => repr varSource

input :: (Ord var, Show var) => var -> repr varSource

not :: (Ord var, Show var) => repr var -> repr varSource

and :: (Ord var, Show var) => repr var -> repr var -> repr varSource

Defined as `and p q = not (not p or not q)`.

or :: (Ord var, Show var) => repr var -> repr var -> repr varSource

Defined as `or p q = not (not p and not q)`.

ite :: (Ord var, Show var) => repr var -> repr var -> repr var -> repr varSource

If-then-else circuit. `ite c t e` returns a circuit that evaluates to `t` when `c` evaluates to true, and `e` otherwise.

Defined as `(c and t) or (not c and f)`.

onlyif :: (Ord var, Show var) => repr var -> repr var -> repr varSource

Defined as `onlyif p q = not p or q`.

iff :: (Ord var, Show var) => repr var -> repr var -> repr varSource

Defined as `iff p q = (p onlyif q) and (q onlyif p)`.

xor :: (Ord var, Show var) => repr var -> repr var -> repr varSource

Defined as `xor p q = (p or q) and not (p and q)`.

Instances

 Circuit Graph Circuit Eval Circuit Tree Circuit Shared

class CastCircuit c whereSource

Instances of `CastCircuit` admit converting one circuit representation to another.

Methods

castCircuit :: (Circuit cOut, Ord var, Show var) => c var -> cOut varSource

Instances

 CastCircuit Tree CastCircuit FrozenShared CastCircuit Shared

## Explicit sharing circuit

newtype Shared v Source

A `Circuit` constructed using common-subexpression elimination. This is a compact representation that facilitates converting to CNF. See `runShared`.

Constructors

 Shared FieldsunShared :: State (CMaps v) CCode

Instances

 CastCircuit Shared Circuit Shared

data FrozenShared v Source

A shared circuit that has already been constructed.

Constructors

 FrozenShared !CCode !(CMaps v)

Instances

 CastCircuit FrozenShared Eq v => Eq (FrozenShared v) Show v => Show (FrozenShared v)

Reify a sharing circuit.

type CircuitHash = IntSource

0 is false, 1 is true. Any positive value labels a logical circuit node.

data CCode Source

A `CCode` represents a circuit element for `Shared` circuits. A `CCode` is a flattened tree node which has been assigned a unique number in the corresponding map inside `CMaps`, which indicates children, if any.

For example, `CAnd i` has the two children of the tuple ```lookup i (andMap cmaps)``` assuming `cmaps :: CMaps v`.

Constructors

 CTrue FieldscircuitHash :: !CircuitHash CFalse FieldscircuitHash :: !CircuitHash CVar FieldscircuitHash :: !CircuitHash CAnd FieldscircuitHash :: !CircuitHash COr FieldscircuitHash :: !CircuitHash CNot FieldscircuitHash :: !CircuitHash CXor FieldscircuitHash :: !CircuitHash COnlyif FieldscircuitHash :: !CircuitHash CIff FieldscircuitHash :: !CircuitHash CIte FieldscircuitHash :: !CircuitHash

Instances

 Eq CCode Ord CCode Read CCode Show CCode

data CMaps v Source

Maps used to implement the common-subexpression sharing implementation of the `Circuit` class. See `Shared`.

Constructors

 CMaps FieldshashCount :: [CircuitHash]Source of unique IDs used in `Shared` circuit generation. Should not include 0 or 1. varMap :: Bimap CircuitHash vMapping of generated integer IDs to variables. andMap :: Bimap CircuitHash (CCode, CCode) orMap :: Bimap CircuitHash (CCode, CCode) notMap :: Bimap CircuitHash CCode xorMap :: Bimap CircuitHash (CCode, CCode) onlyifMap :: Bimap CircuitHash (CCode, CCode) iffMap :: Bimap CircuitHash (CCode, CCode) iteMap :: Bimap CircuitHash (CCode, CCode, CCode)

Instances

 Eq v => Eq (CMaps v) Show v => Show (CMaps v)

A `CMaps` with an initial `hashCount` of 2.

## Explicit tree circuit

data Tree v Source

Explicit tree representation, which is a generic description of a circuit. This representation enables a conversion operation to any other type of circuit. Trees evaluate from variable values at the leaves to the root.

Constructors

 TTrue TFalse TLeaf v TNot (Tree v) TAnd (Tree v) (Tree v) TOr (Tree v) (Tree v) TXor (Tree v) (Tree v) TIff (Tree v) (Tree v) TOnlyIf (Tree v) (Tree v) TIte (Tree v) (Tree v) (Tree v)

Instances

 CastCircuit Tree Circuit Tree Eq v => Eq (Tree v) Ord v => Ord (Tree v) Show v => Show (Tree v)

foldTree :: (t -> v -> t) -> t -> Tree v -> tSource

### Circuit simplification

simplifyTree :: Tree v -> Tree vSource

Performs obvious constant propagations.

## Explicit graph circuit

data Graph v Source

A circuit type that constructs a `Graph` representation. This is useful for visualising circuits, for example using the `graphviz` package.

Instances

 Circuit Graph

shareGraph :: (DynGraph gr, Eq v, Show v) => FrozenShared v -> gr (FrozenShared v) (FrozenShared v)Source

Given a frozen shared circuit, construct a `DynGraph` that exactly represents it. Useful for debugging constraints generated as `Shared` circuits.

data NodeType v Source

Node type labels for graphs.

Constructors

 NInput v NTrue NFalse NAnd NOr NNot NXor NIff NOnlyIf NIte

Instances

 Eq v => Eq (NodeType v) Ord v => Ord (NodeType v) Read v => Read (NodeType v) Show v => Show (NodeType v)

data EdgeType Source

Constructors

 ETest the edge is the condition for an `ite` element EThen the edge is the then branch for an `ite` element EElse the edge is the else branch for an `ite` element EVoid no special annotation

Instances

 Eq EdgeType Ord EdgeType Read EdgeType Show EdgeType

## Circuit evaluator

type BEnv v = Map v BoolSource

newtype Eval v Source

A circuit evaluator, that is, a circuit represented as a function from variable values to booleans.

Constructors

 Eval FieldsunEval :: BEnv v -> Bool

Instances

 Circuit Eval

runEval :: BEnv v -> Eval v -> BoolSource

Evaluate a circuit given inputs.

## Convert circuit to CNF

data CircuitProblem v Source

A circuit problem packages up the CNF corresponding to a given `FrozenShared` circuit, and the mapping between the variables in the CNF and the circuit elements of the circuit.

Constructors

 CircuitProblem FieldsproblemCnf :: CNF problemCircuit :: FrozenShared v problemCodeMap :: Bimap Var CCode

toCNF :: (Ord v, Show v) => FrozenShared v -> CircuitProblem vSource

Produces a CNF formula that is satisfiable if and only if the input circuit is satisfiable. Note that it does not produce an equivalent CNF formula. It is not equivalent in general because the transformation introduces variables into the CNF which were not present as circuit inputs. (Variables in the CNF correspond to circuit elements.) Returns equisatisfiable CNF along with the frozen input circuit, and the mapping between the variables of the CNF and the circuit elements.

The implementation uses the Tseitin transformation, to guarantee that the output CNF formula is linear in the size of the circuit. Contrast this with the naive DeMorgan-laws transformation which produces an exponential-size CNF formula.

Projects a funsat `Solution` back into the original circuit space, returning a boolean environment containing an assignment of all circuit inputs to true and false.