picosat-0.1.6: Bindings to the PicoSAT solver

Picosat

Description

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

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

Synopsis

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

type Picosat = Ptr () Source #

data Solution Source #

Constructors

 Solution [Int] Unsatisfiable Unknown
Instances
 Source # Instance detailsDefined in Picosat Methods Source # Instance detailsDefined in Picosat Methods(<) :: Solution -> Solution -> Bool #(>) :: Solution -> Solution -> Bool # Source # Instance detailsDefined in Picosat MethodsshowList :: [Solution] -> ShowS #

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

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