Picosat

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 to the SAT solver using the solve function either in IO or ST monad.

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
import Control.Monad.ST

main :: [Int]
main = runST $ do
  solveAllST [[1,2]]
  -- [Solution [1,2],Solution [-1,2],Solution [1,-2]]

For a higher level interface see: http://hackage.haskell.org/package/picologic

Documentation

solve :: [[Int]] -> IO Solution

Solve a list of CNF constraints yielding the first solution.

solveAll :: [[Int]] -> IO [Solution]

Solve a list of CNF constraints yielding all possible solutions.

unsafeSolve :: [[Int]] -> Solution

unsafeSolveAll :: [[Int]] -> [Solution]

data Solution

Constructors

Solution [Int]

Unsatisfiable

Unknown

Instances

Eq Solution

Show Solution