Heuristic solvers for boolean satisfaction problems.
Author CarloLucibello
5 Stars
Updated Last
1 Year Ago
Started In
September 2016


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 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)


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.