# 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
- Maxime Bouton -@MaximeBouton