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 variables`verbose`

- 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)`

- Returns a solution if the problem is satisfiable. Satisfiable solutions are represented as a vector of signed integers. If the problem is not satisfiable the method returns an
`: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)`

- Returns an iterable object over all solutions. When a user-defined propagation limit is specified, the iterator may not produce all feasible solutions.
`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.

- Jake Bolewski - @jakebolewski
- Carlo Lucibello - @CarloLucibello

11/28/2014

5 months ago

39 commits