# 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:

- Haskell plattform with
`ghc >= 7.10.2`

- Minisat
- Satchmo-core

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

`True`

denotes the value of the parameter`c`

in`constraint`

`complete`

denotes that the complete search space should be considered when searching a solution (note that the search space in this example contains only four elements`(False,False)`

,`(False,True)`

,`(True,False)`

, and`(True,True)`

)`encConstraint`

denotes the compiled constraint

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

*RNA Design by Program Inversion via SAT solving*at WCB 2013 (Proceedings)*Propositional Encoding of Constraints over Tree-Shaped Data*at WFLP 2013*SAT compilation for Termination Proofs via Semantic Labelling*at WST 2013 (Proceedings)