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

If you intend to solve a set of similar CNFs think about using Picosat's incremental interface. It allows to push and pop sets of clauses, as well as solving under assumptions.

import Picosat (evalScopedPicosat, addBaseClauses,
                withScopedClauses, scopedAllSolutions,
                scopedSolutionWithAssumptions)

main :: IO [Int]
main =
  evalScopedPicosat $ do
    addBaseClauses [[1, 2, 3]]
    -- == [Solution [1,2,3],
    --     Solution [1,2,-3],
    --     Solution [1,-2,3],
    --     Solution [1,-2,-3],
    --     Solution [-1,-2,3],
    --     Solution [-1,2,-3],
    --     Solution [-1,2,3]]

    withScopedClauses [[-2,-3]] $ do
      sol <- scopedAllSolutions
      -- ==   [Solution [-1,2,-3],
      --       Solution [-1,-2,3],
      --       Solution [1,-2,-3],
      --       Solution [1,-2,3],
      --       Solution [1,2,-3]]

    addBaseClauses [[-1,-3]]

    withScopedClauses [[-1,-2], [1,-3]] $ do
      sol <- scopedSolutionWithAssumptions [1]

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]

type Picosat = Ptr ()

data Solution

Constructors

Solution [Int]

Unsatisfiable

Unknown

Instances

Eq Solution

Methods

(==) :: Solution -> Solution -> Bool

(/=) :: Solution -> Solution -> Bool

Ord Solution

Methods

compare :: Solution -> Solution -> Ordering

(<) :: Solution -> Solution -> Bool

(<=) :: Solution -> Solution -> Bool

(>) :: Solution -> Solution -> Bool

(>=) :: Solution -> Solution -> Bool

max :: Solution -> Solution -> Solution

min :: Solution -> Solution -> Solution

Show Solution

Methods

showsPrec :: Int -> Solution -> ShowS

show :: Solution -> String

showList :: [Solution] -> ShowS

evalScopedPicosat :: PS a -> IO a

addBaseClauses :: [[Int]] -> PS ()

withScopedClauses :: [[Int]] -> PS a -> PS a

scopedAllSolutions :: PS [Solution]

scopedSolutionWithAssumptions :: [Int] -> PS Solution