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