CO4 enables a subset of Haskell to be used as a constraint specification language through transformation into a satisfiability problem in propositional logic.
- [Haskell plattform] (http://www.haskell.org/platform/) with
ghc >= 7.8.2
- [Minisat] (https://github.com/niklasso/minisat.git)
- [Minisat C bindings] (https://github.com/niklasso/minisat-c-bindings)
- [Minisat Haskell bindings] (https://github.com/niklasso/minisat-haskell-bindings)
- [Satchmo-core] (https://github.com/apunktbau/satchmo-core)
All other dependencies are available on Hackage and will be installed by cabal during the next step.
cabal install
[test/CO4/Example/BinaryStandalone.hs] (https://github.com/apunktbau/co4/tree/master/test/CO4/Example/BinaryStandalone.hs) implements addition and multiplication of binary values:
fullAdder :: Bit -> Bit -> Bit -> (Bit,Bit)
fullAdder a b carry =
let xorAB = xor a b
in
( xor xorAB carry
, xor (a && b) (carry && xorAB)
)
halfAdder :: Bit -> Bit -> (Bit,Bit)
halfAdder a b = (xor a b, a && b)
mult :: Nat -> Nat -> (Nat,Bit)
mult a b = case a of
[] -> ([],False)
(x:xs) ->
let multResult = mult xs b
shiftResult = withCarry shiftRight multResult
in
case x of
False -> shiftResult
True -> withCarry (add b) shiftResult
...
The toplevel constraint constraint r (a,b)
is satisfied if
a * b = r
(without an overflow) anda > 1
andb > 1
So:
constraint r (a,b) = case mult a b of
(result,carry) -> and [ result == r
, not (trivial a)
, not (trivial b)
, not carry
]
[test/CO4/Example/Binary.hs] (https://github.com/apunktbau/co4/tree/master/test/CO4/Example/Binary.hs) loads and compiles [test/CO4/Example/BinaryStandalone.hs] (https://github.com/apunktbau/co4/tree/master/test/CO4/Example/BinaryStandalone.hs) using Template-Haskell:
$( compileFile [ImportPrelude] "test/CO4/Example/BinaryStandalone.hs" )
Every definition d
of the original program is compiled to an encoded
definition encD
, i.e. the compiled constraint system is encConstraint
.
As we're using definitions of Haskell's prelude (map
,foldl
,etc.),
we pass the compiler flag ImportPrelude
.
Next, we need to setup an allocator for the unknown values.
Allocators may represent the whole problem domain (complete
) or certain subsets.
Because we are dealing with lists, complete
is no option:
we have to restrict the problem domain to a finite set.
So we fix the width of the binary values to 8 bit:
bitWidth = 8
uBinary = uList bitWidth complete
As constraint
is a constraint over a pair of naturals, the final allocator is
allocator = knownTuple2 uBinary uBinary
Finally, we want to solve the compiled constraint system encConstraint
.
CO4 provides several solving functions, e.g.
solveAndTestP :: k -> TAllocator a -> ParamConstraintSystem -> (k -> a -> b) -> IO (Maybe a)
solves a parametrized constraint system with
k
being the parameterTAllocator a
being an allocator for values of typea
ParamConstraintSystem
being the parametrized constraint system(k -> a -> b)
being the original constraint system. The found solution is checked against this function in order to verify the solution.
In the main constraint
we seek a factorization for a given natural number x
of
bit-width bitWidth
using the previously defined allocator:
solution <- solveAndTestP (toBinary (Just bitWidth) x) allocator encConstraint constraint
If there is a factorization, we want to decode the factors to decimal numbers:
result :: Int -> IO (Maybe (Int,Int))
result x = do
solution <- solveAndTestP (toBinary (Just bitWidth) x) allocator encConstraint constraint
case solution of
Nothing -> return Nothing
Just (a,b) -> return $ Just (fromBinary a, fromBinary b)
We call result
in a ghci session to find a factorization of 143:
$ ghci -isrc -itest test/CO4/Example/Binary.hs
*CO4.Example.Binary> result 143
Start producing CNF
Allocator: #variables: 34, #clauses: 18
Cache hits: 162 (10%), misses: 1441 (89%)
Toplevel: #variables: 1, #clauses: 3
CNF finished
#variables: 3049, #clauses: 10155, #literals: 28409, clause density: 3.3306001967858316
#variables (Minisat): 3049, #clauses (Minisat): 10154, clause density: 3.3302722204001314
#clauses of length 1: 1
#clauses of length 2: 2066
#clauses of length 3: 8086
#clauses of length 9: 2
Starting solver
Solver finished in 1.6666e-2 seconds (result: True)
Starting decoder
Decoder finished
Test: True
Just (13,11)
For more examples see [test/CO4/Example] (https://github.com/apunktbau/co4/tree/master/test/CO4/Example).
- RNA Design by Program Inversion via SAT solving at [WCB 2013] (http://cp2013.a4cp.org/workshops/wcb) ([Proceedings] (http://cp2013.a4cp.org/sites/default/files/uploads/WCB13_proceedings.pdf))
- Propositional Encoding of Constraints over Tree-Shaped Data at [WFLP 2013] (http://www-ps.informatik.uni-kiel.de/wflp2013/)
- SAT compilation for Termination Proofs via Semantic Labelling at [WST 2013] (http://www.imn.htwk-leipzig.de/WST2013/) ([Proceedings] (http://www.imn.htwk-leipzig.de/WST2013/papers/wst13.pdf))