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