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.
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
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
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
solveP True complete encConstraint :: IO (Maybe (Bool,Bool))
Truedenotes the value of the parameter
completedenotes that the complete search space should be considered when searching a solution (note that the search space in this example contains only four elements
encConstraintdenotes the compiled constraint
:: 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.