# SAT.jl

Heuristic algorithms based on message passing for solving large instances of boolean satisfaction problems, written in julia. Consider using PicoSAT.jl if you are looking for an exact solver.

## Basic usage

```
using SAT
cnf = randomcnf(N=1000, k=3, α=0.5) # generate a random k-SAT instance
σ = solve(cnf)
```

The solution `σ`

will be a vector of `N`

ints taking values `-1`

or `+1`

.

## Formulas

Formulas in conjunctive normal form (CNF) can be either read/written to files

```
cnf = readcnf("formula.cnf")
writecnf("formula.cnf", cnf)
```

or randomly generated from the k-SAT ensemble

`cnf = randomcnf(N=1000, k=4, α=0.5, seed=17)`

## Solvers

### BP + reinforcement (default)

Solve random instance with Belief Propagation (BP) inspired procedures.
`r`

is the initial value of the reinforcement parameter (`r=0`

default).
`rstep`

determines its moltiplicative increment.

`σ = solve(cnf, rstep=0.001, maxiters=1000);`

If having errors or unable to find a solution, try to reduce `rstep`

.

### decimation

TODO