Safe Haskell | None |
---|---|
Language | Haskell2010 |
We wish to find a solution that satisifes the following logical condition.
(A v ¬B v C) ∧ (B v D v E) ∧ (D v F)
We can specify this as a zero-terminated lists of integers, with integers mapping onto the variable as ordered in the condition and with integer negation corresponding to logical negation of the specific clause.
1 -2 3 0 2 4 5 0 4 6 0
We feed this list of clauses to the SAT solver using the solve
function.
import Picosat main :: IO [Int] main = do solve [[1, -2, 3], [2,4,5], [4,6]] -- Solution [1,-2,3,4,5,6]
The solution given we can interpret as:
1 A -2 ~B 3 C 4 D 5 E 6 F
To generate all satisfiable solutions, use solveAll
function.:
import Picosat main :: IO [Int] main = solveAll [[1,2]] -- [Solution [1,2],Solution [-1,2],Solution [1,-2]]
For a higher level interface see: http://hackage.haskell.org/package/picologic