picosat-0.1.2: 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

Synopsis

# Documentation

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

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.

data Solution Source

Constructors

 Solution [Int] Unsatisfiable Unknown

Instances

 Eq Solution Show Solution