picosat alternatives and similar packages
Based on the "Logic" category.
Alternatively, view picosat alternatives based on common mentions on social networks and blogs.

tamarinprover
Main source code repository of the Tamarin prover for security protocol verification. 
atphaskell
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning" 
logicclasses
Framework for propositional and first order logic, theorem proving 
obdd
pure Haskell implementation of reduced ordered binary decision diagrams 
structuralinduction
SII: Structural Induction Instantiator over any strictlypositive algebraic data type. 
g4ipprover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip 
tpdb
parser and prettyprinter for TPDB syntax (termination problem data base) 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Static code analysis for 29 languages.
Do you think we are missing an alternative of picosat or a related project?
README
Haskell PicoSAT
haskellpicosat are Haskell bindings to the PicoSAT solver, written in C. It reads in clauses in CNF ( ConjunctiveNormal Form ) and returns a solution which satisfies the clauses.
The most notable distinction of this binding is that the SAT solver library is included with the cabal package so you shouldn't need to install anything but this package to get going. It's also notably faster than a pure Haskell solution at solving very large constraint problems.
Installing
$ cabal install picosat
Usage
If we have a table of variables representing logical statements we can enumerate them with integers.
A 1
B 2
C 3
D 4
E 5
F 6
Then the clause can be written as sequences of positive integers (assertion) and negative integers (negation):
(A v ¬B v C)
1 2 3 0
(B v D v E)
2 4 5 0
(D V F)
4 6 0
Solutions to a statement of the form:
(A v ¬B v C) ∧ (B v D v E) ∧ (D v F)
Can be written as zeroterminated lists of integers:
1 2 3 0
2 4 5 0
4 6 0
To use the Haskell bindings simply pass a list of clauses to
the solve
function, this will return either the solution or
Unsatisfiable
or Unknown
.
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 possible solutions we repeatedly feed the negated solution to the solver yielding which is
implemented with the solveAll
function which yields a sequence of solutions.
import Picosat
main :: IO [Int]
main = solveAll [[1,2]]
 [Solution [1,2],Solution [1,2],Solution [1,2]]
For a more complicated example a Sudoku solver is included as an example.
License
PicoSAT itself is included and is also licensed the MIT license. Copyright (c) 2006  2012, Armin Biere, Johannes Kepler University.
Released under the MIT License. Copyright (c) 20132020, Stephen Diehl
*Note that all licence references and agreements mentioned in the picosat README section above
are relevant to that project's source code only.