CO4 - COmplexity COncerned COnstraint COmpiler

CO4 is a constraint solver that enables a syntactically subset of Haskell to be used as a constraint specification language. Constraints are solved by Minisat after compiling them into satisfiability problems in propositional logic.

Building

The following tools are required in order to build CO4:

All other dependencies are available on Hackage and will be installed by cabal. Get CO4’s sources and build via:

cabal configure
cabal build

Example

test/CO4/Example/Adder.hs specifies an adder curcuit:

halfAdder :: Bool -> Bool -> (Bool,Bool)
halfAdder a b = (xor2 a b, a && b)

fullAdder :: Bool -> Bool -> Bool -> (Bool,Bool)
fullAdder a b c = case halfAdder a b of
  (s1,c1) -> case halfAdder s1 c of
    (s2,c2) -> (s2, c1 || c2)

Furthermore, this module specifies a parameterized constraint over pairs (a,b) of Boolean values:

constraint c (a,b) = not $ snd $ fullAdder a b c

For a given parameter c, the constraint is satisfied if fullAdder applied to a, b, and c does not result in a positive carry value. Load test/CO4/Example/Adder.hs with via:

ghci -isrc test/CO4/Example/Adder.hs

Loading this module compiles the constraint into an intermediate representation that is bound to the identifier encConstraint. Solve encConstraint

solveP True complete encConstraint :: IO (Maybe (Bool,Bool))

where

The signature :: IO (Maybe (Bool,Bool)) is necessary to resolve type ambiguities.

Solving the constraint leads to the following output:

$ ghci -isrc test/CO4/Example/Adder.hs
> solveP True complete encConstraint :: IO (Maybe (Bool,Bool))
Start producing CNF
Number of shared values: 0
Allocator: #variables: 2, #clauses: 0
Cache hits: 0 (0%), misses: 10 (100%)
Toplevel: #variables: 0, #clauses: 1
CNF finished
#variables: 6, #clauses: 13, #literals: 31, clause density: 2.16666666665
#variables (Minisat): 6, #clauses (Minisat): 12, clause density: 2.0
#clauses of length 1:   1
#clauses of length 2:   6
#clauses of length 3:   6

Starting solver
Solver finished in 0.0 seconds (result: True)
Starting decoder
Decoder finished
Just (False,False)

The last line shows the actual result: (False,False) solves the above constraint for paramter c = True. Additionally, statistics about the generated propositional problem are printed. For the above constraint CO4 generates a propositional formula in conjunctive normal form (CNF) with 6 variables, 13 clauses, and 31 literals.

For more complex examples see test/CO4/Example.

Applications