SAT-solver-sample.lua

-- note: this sample file requires picosat or minisat
USE_PICOSAT = true
USE_MINISAT = false

dofile("SAT-solver-framework.lua")
NewVar("a")
NewVar("b", 2)
NewVar("c", {2,3})
AddSimpleClause{Var.a, true}
AddIfThenClause(
    "if ALL", {
    Var.a, true},
    "then ONE", {
    Var.b[1], true}
)
AddSimpleClause{Var.a, false, Var.b[1], false, Var.b[2], true}
AddSimpleClause{Var.c[1][1], true}
AddSimpleClause{Var.c[1][2], true}
AddSimpleClause{Var.c[2][1], true}
AddSimpleClause{Var.c[2][1], false, Var.c[2][2], false}
AddIfAndOnlyIfClause(
    "ALL of", {
    Var.c[1][3], true},
    "if and only if",
    "ALL of", {
    Var.c[2][3], true}
)
WriteSATfile()
if USE_PICOSAT then
    os.execute("picosat satfile.cnf >solutionfile")
elseif USE_MINISAT then
    os.execute("minisat satfile.cnf solutionfile")
end
ParseSolution()
PrintSolution()
print("again: c[1][1]=="..tostring(Sol.c[1][1]))