PicoSAT.jl provides Julia bindings to the popular SAT solver picosat by Armin Biere. It is based off the Python pycosat and Go pigosat bindings written by Ilan Schnell and Willam Schwartz.
To install, run Pkg.add("PicoSAT")
in Julia. The entire picosat library (v960) is shipped with the package to make building the library easier. Windows builds are currently not supported at the moment.
The PicoSAT
module exports two functions solve
and itersolve
. Both functions take an iterable of clauses as a required argument. Each clause is represented as an iterable of non-zero integers.
Both methods take the following optional keyword arguments:
vars
- the number of variablesverbose
- prints solver logs to STDOUT
when verbose > 0
with increasing detail.proplimit
- helps to bound the execution time. The number of propagations and the solution time are roughly linearly related. A value of 0 (default) allows for an unbounded number of propagations.solve(clauses; vars::Integer=-1, verbose::Integer=0, proplimit::Integer=0)
:unsatisfiable
symbol. If a solution cannot be found within the defined propagation limit, an :unknown
symbol is returned.
julia> import PicoSAT
julia> cnf = Any[[1, -5, 4], [-1, 5, 3, 4], [-3, -4]];
julia> PicoSAT.solve(cnf)
5-element Array{Int64,1}:
1
-2
-3
-4
5
The absolute values of the solution vector represent the ith variable. The sign of the ith variable represents the boolean values true
(+) and false
(-).
itersolve(clauses; vars::Integer=-1, verbose::Integer=0, proplimit::Integer=0)
julia> import PicoSAT
julia> cnf = Any[[1, -5, 4], [-1, 5, 3, 4], [-3, -4]];
julia> PicoSAT.itersolve(cnf)
julia> for sol in PicoSAT.itersolve(cnf)
println(sol)
end
[1,-2,-3,-4,5]
[1,-2,-3,4,-5]
[1,-2,-3,4,5]
[1,-2,3,-4,-5]
...
PicoSAT.jl
and the original picosat
C-library are licensed under the MIT "Expat" license.
11/28/2014
27 days ago
60 commits