18

2

8

5

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

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

11/28/2014

27 days ago

60 commits