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

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]

## Synopsis

- solve :: [[Int]] -> IO Solution
- solveAll :: [[Int]] -> IO [Solution]
- unsafeSolve :: [[Int]] -> Solution
- unsafeSolveAll :: [[Int]] -> [Solution]
- type Picosat = Ptr ()
- data Solution
- = Solution [Int]
- | Unsatisfiable
- | Unknown

- evalScopedPicosat :: PS a -> IO a
- addBaseClauses :: [[Int]] -> PS ()
- withScopedClauses :: [[Int]] -> PS a -> PS a
- scopedAllSolutions :: PS [Solution]
- scopedSolutionWithAssumptions :: [Int] -> PS Solution

# Documentation

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

Solve a list of CNF constraints yielding the first solution.

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

Solve a list of CNF constraints yielding all possible solutions.

unsafeSolve :: [[Int]] -> Solution Source #

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

evalScopedPicosat :: PS a -> IO a Source #

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

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

scopedAllSolutions :: PS [Solution] Source #

scopedSolutionWithAssumptions :: [Int] -> PS Solution Source #