SAT-solver-framework.lua

function deepcopy(v)
    if(type(v)=="table") then
        local t = {}
        local key, val
        for key, val in pairs(t) do
            t[key] = deepcopy(val)
        end
        return t
    else
        return v
    end
end

total_number_of_variables = 0

Var = {}
pvar = {}
num_to_var = {}
function NewVar(name, entries, print_entries)
    if print_entries==nil then print_entries=true end
    assert(print_entries == true or print_entries == false or
        print_entries == "true" or print_entries == "false",
        "print_entries was wrong! (Maybe you wanted NewVar("..
        name..",{"..tostring(entries)..","..tostring(print_entries).."})   ?")

    local tab = {}
    local ctab, ulim
    if type(entries)=="table" then
        temp = {}
        for i=0,#entries do
            temp[i] = 1
        end
        while(true) do
            ctab = tab
            for i=1,#entries-1 do
                if type(ctab[temp[i]])=="nil" then ctab[temp[i]]={} end
                ctab = ctab[temp[i]]
            end
            for j=1,entries[#entries] do
                total_number_of_variables = total_number_of_variables + 1
                ctab[j] = total_number_of_variables

                local temp2 = {}
                for i=1,#entries-1 do temp2[i]=temp[i] end
                temp2[#entries] = j
                num_to_var[total_number_of_variables] = {
                    name = name, entry = temp2
                }
            end
            temp[#entries-1] = temp[#entries-1] + 1

            ulim = #entries-1
            while(ulim > 0 and temp[ulim] > entries[ulim]) do
                temp[ulim] = 1
                ulim = ulim - 1
                temp[ulim] = temp[ulim] + 1
            end
            if ulim == 0 then break end
        end
        Var[name] = tab
    elseif type(entries)=="number" then
        for i=1,entries do
            total_number_of_variables = total_number_of_variables + 1
            tab[i]= total_number_of_variables
            num_to_var[total_number_of_variables] = {
                name = name, entry = i
            }
        end
        Var[name] = tab
    elseif type(entries)=="nil" then
        total_number_of_variables = total_number_of_variables + 1
        Var[name] = total_number_of_variables
        num_to_var[total_number_of_variables] = {
            name = name
        }
    end
    pvar[name] = print_entries
end

total_number_of_clauses = 0
clause = {}

function CheckClause(cl)
    assert(type(cl) == "table",
            "ERROR: cl should be a table")

    assert(#cl > 0, "ERROR: inserting an empty table! (pretty pointless, it's never solvable)")
    for i=1,#cl,2 do
        assert(type(cl[i]) == "number",
            "ERROR: cl["..i.."]="..tostring(cl[i])..", but should be a number")
        assert(type(cl[i+1]) == "boolean",
            "ERROR: cl["..(i+1).."]="..tostring(cl[i+1])..", but should be true or false")
    end
end

function AddSimpleClause(cl)
    total_number_of_clauses = total_number_of_clauses + 1
    CheckClause(cl)
    clause[total_number_of_clauses] = cl
end

function AddIfThenClause(str_if, cl1, str_then, cl2)
    assert(str_if=="if" or str_if=="if ALL" or str_if=="if ONE",
        "bad argument for str_if, it is "..str_if..", but must be"..
        "\n  if"..
        "\nOR"..
        "\n  if ALL"..
        "\nOR"..
        "\n  if ONE")
    assert(str_then=="then" or str_then=="then ALL" or str_then=="then ONE",
        "bad argument for str_then, it is "..str_then..", but must be"..
        "\n  then"..
        "\nOR"..
        "\n  then ALL"..
        "\nOR"..
        "\n then ONE")

    CheckClause(cl1)
    CheckClause(cl2)

    local invert_cl1 = {}
    for i=1,#cl1,2 do
        invert_cl1[i] = cl1[i]
        invert_cl1[i + 1] = not cl1[i + 1]
    end

    if str_if=="if" or str_if=="if ALL" then

        if str_then=="then" or str_then=="then ALL" then

            for i=1,#cl2,2 do
                local t = {}
                for j=1,#invert_cl1 do
                    t[j] = invert_cl1[j]
                end
                t[#t+1] = cl2[i]
                t[#t+1] = cl2[i+1]
                AddSimpleClause(t)
            end

        elseif str_then=="then ONE" then

            local t = {}
            for j=1,#invert_cl1 do
                t[j] = invert_cl1[j]
            end
            for j=1,#cl2 do
                t[#t+1] = cl2[j]
            end
            AddSimpleClause(t)
        end

    elseif str_if=="if ONE" then

        if str_then=="then" or str_then=="then ALL" then

            for i=1,#invert_cl1,2 do for j=1,#cl2,2 do
                AddSimpleClause{
                    invert_cl1[i], invert_cl1[i+1],
                    cl2[j], cl2[j+1]}
            end end

        elseif str_then=="then ONE" then

            for i=1,#invert_cl1,2 do
                local t = {invert_cl1[i], invert_cl1[i+1]}
                for j=1,#cl2 do
                    t[#t+1] = cl2[j]
                end
                AddSimpleClause(t)
            end

        end
    end
end

function AddIfAndOnlyIfClause(str_cl1, cl1, str_ifandonlyif, str_cl2, cl2)
    assert(str_cl1=="ONE of" or str_cl1=="ALL of",
        "str_cl1 not specified, must be"..
        "\n   ONE of"..
        "\nOR"..
        "\n   ALL of")
    assert(str_cl2=="ONE of" or str_cl2=="ALL of",
        "str_cl2 not specified, must be"..
        "\n   ONE of"..
        "\nOR"..
        "\n   ALL of")
    assert(str_ifandonlyif=="if and only if",
        "str_ifandonlyif must be exactly the following string:"..
        "\n   if and only if")

    CheckClause(cl1)
    CheckClause(cl2)

    if str_cl1=="ALL of" then
        if str_cl2=="ALL of" then
            AddIfThenClause("if ALL", cl1, "then ALL", cl2)
            AddIfThenClause("if ALL", cl2, "then ALL", cl1)
        elseif str_cl2=="ONE of" then
            AddIfThenClause("if ALL", cl1, "then ONE", cl2)
            AddIfThenClause("if ONE", cl2, "then ALL", cl1)
        end
    elseif str_cl1=="ONE of" then
        if str_cl2=="ALL of" then
            AddIfThenClause("if ONE", cl1, "then ALL", cl2)
            AddIfThenClause("if ALL", cl2, "then ONE", cl1)
        elseif str_cl2=="ONE of" then
            AddIfThenClause("if ONE", cl1, "then ONE", cl2)
            AddIfThenClause("if ONE", cl2, "then ONE", cl1)
        end
    end
end

function UnitClause(var, bool)
    AddSimpleClause{var, bool}
end

function NewClause()
    return {}
end

function ExtendClause(cl, var, bool)
    assert(type(var)=="number", "var=="..tostring(var).." but should be a number")
    assert(type(bool)=="boolean", "bool=="..tostring(bool).." but should be true or false")
    cl[#cl + 1] = var
    cl[#cl + 1] = bool
end

function WriteSATfile()
    file = io.open("satfile.cnf", "w")
    file.write(file, "p cnf "..total_number_of_variables.." "..total_number_of_clauses.."\n")
    local s = ""
    for i=1,total_number_of_clauses do
        s = ""
        local j = 1
        while(clause[i][j] ~= nil and clause[i][j+1] ~= nil) do
            if not clause[i][j+1] then s = s .. "-" end
            s = s .. clause[i][j] .. " "
            j = j + 2
        end
        file.write(file, s.."0\n")
    end
    file.close(file)
end

function ParseSolution()
    file = io.open("solutionfile", "r")
    Sol = {}
    local s, lin
    for lin in file.lines(file) do for s in string.gmatch(lin, "[%d%-]+") do
        local b
        s = s + 0
        if s > 0 then
            b = true
        elseif s < 0 then
            b = false
            s = -s
        else
            break
        end

        local con = num_to_var[s]
        local name = con.name
        local entry = con.entry
        if type(entry)=="nil" then
            Sol[name] = b
        elseif type(entry)=="number" then
            entry = entry + 0
            if type(Sol[name])=="nil" then
                Sol[name] = {}
            end
            Sol[name][entry] = b
        elseif type(entry)=="table" then
            if type(Sol[name])=="nil" then
                Sol[name] = {}
            end
            local v = Sol[name]
            for j = 1, #entry - 1 do
                if type(v[entry[j]])=="nil" then
                    v[entry[j]] = {}
                end
                v = v[entry[j]]
            end
            v[entry[#entry]] = b
        end
    end end
end

function PrintSolution()

    local function PrintVar(s, v, p)
        if p==false then return end
        if type(v)=="number" then
            print(s..": ".." unknown")
        elseif type(v)=="boolean" then
            if p==nil or p==true or tostring(v)==tostring(p) then print(s..": "..tostring(v)) end
        elseif type(v)=="table" then
            for key, val in pairs(v) do
                PrintVar(s.."["..key.."]", val, p)
            end
        end
    end
    for key, val in pairs(Sol) do
        PrintVar(key, val, pvar[key])
    end
end