picosat-0.1.6: Bindings to the PicoSAT solver

Safe HaskellNone
LanguageHaskell2010

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

    addBaseClauses [[-1,-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
Eq Solution Source # 
Instance details

Defined in Picosat

Ord Solution Source # 
Instance details

Defined in Picosat

Show Solution Source # 
Instance details

Defined in Picosat

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

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