funsat-0.6.0: A modern DPLL-style SAT solver




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


Circuit type class

class Circuit repr whereSource

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


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

class CastCircuit c whereSource

Instances of CastCircuit admit converting one circuit representation to another.


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

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.




unShared :: State (CMaps v) CCode

data FrozenShared v Source

A shared circuit that has already been constructed.


FrozenShared !CCode !(CMaps v) 

runShared :: Shared v -> FrozenShared vSource

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.

data CMaps v Source

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




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)


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.


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) 


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.


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.


NInput v 


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

data EdgeType Source



the edge is the condition for an ite element


the edge is the then branch for an ite element


the edge is the else branch for an ite element


no special annotation

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.




unEval :: BEnv v -> Bool


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.

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.