PicoSAT.jl

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.

Installation

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.

Usage

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

License

PicoSAT.jl and the original picosat C-library are licensed under the MIT "Expat" license.

Contributors

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