Funsat.Circuit

Contents

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.

The implementation for this module was adapted from http://okmij.org/ftp/Haskell/DSLSharing.hs.

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
Fields unShared :: 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)

runShared :: Shared v -> FrozenShared vSource

Reify a sharing circuit.

type CircuitHash = Int Source

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

falseHash :: CircuitHash Source

trueHash :: CircuitHash Source

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
Fields circuitHash :: !CircuitHash
CFalse
Fields circuitHash :: !CircuitHash
CVar
Fields circuitHash :: !CircuitHash
CAnd
Fields circuitHash :: !CircuitHash
COr
Fields circuitHash :: !CircuitHash
CNot
Fields circuitHash :: !CircuitHash
CXor
Fields circuitHash :: !CircuitHash
COnlyif
Fields circuitHash :: !CircuitHash
CIff
Fields circuitHash :: !CircuitHash
CIte
Fields circuitHash :: !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

Fields

hashCount :: [CircuitHash]: Source of unique IDs used in Shared circuit generation. Should not include 0 or 1.
varMap :: Bimap CircuitHash v: Mapping 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)

emptyCMaps :: CMaps vSource

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

runGraph :: DynGraph gr => Graph v -> gr (NodeType v) EdgeType Source

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 Bool Source

newtype Eval v Source

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

Constructors

Eval
Fields unEval :: BEnv v -> Bool

Instances

Circuit Eval

runEval :: BEnv v -> Eval v -> Bool Source

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
Fields problemCnf :: 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.

projectCircuitSolution :: Ord v => Solution -> CircuitProblem v -> BEnv vSource

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.