sat-solver-framework.lua

if not USE_WINDOWS and not USE_LINUX then
	error("you must specify the system, some code here is system dependant!")
end

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 = {}
num_to_var = {}
function NewVar(name, 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
end

total_number_of_clauses = 0
clause = {}

function CheckClause(cl)
	assert(type(cl) == "table",
			"ERROR: cl should be a table")
	for i=1,#cl,2 do
		assert(type(cl[i+1]) == "boolean",
			"ERROR: cl["..(i+1).."]="..tostring(cl[i+1])..", but should be true or false")
		assert(type(cl[i]) == "number",
			"ERROR: cl["..i.."]="..tostring(cl[i])..", but should be a number")
	end
end

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

	if max_clauses ~= nil and #clause >= max_clauses then
		print(total_number_of_clauses.." clauses reached, writing...")
		local s = ""
		for i=1,#clause 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
			clausefile.write(clausefile, s.."0\n")
		end
		clause = {}
		collectgarbage()
		print("done!")
	end
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

max_clauses = nil
function StartAutoWrite(new_max_clauses)
	max_clauses = new_max_clauses
	clausefile = io.open("satfile-CLAUSES.cnf", "w")
end

function WriteSATfile()
	file = io.open("satfile-START.cnf", "w")
	file.write(file, "p cnf "..total_number_of_variables.." "..total_number_of_clauses.."\n")
	local s = ""
	for i=1,#clause 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)

	if max_clauses == nil then
		if USE_WINDOWS then
			os.execute("rename satfile-START.cnf satfile.cnf")
		elseif USE_LINUX then
			os.execute("mv satfile-START.cnf satfile.cnf")
		else
			error("function not implemented for your system!")
		end
	else
		clausefile.close(clausefile)
		if USE_WINDOWS then
			os.execute("copy /B satfile-START.cnf + satfile-CLAUSES.cnf satfile.cnf")
			os.execute("del satfile-START.cnf")
			os.execute("del satfile-CLAUSES.cnf")
		elseif USE_LINUX then
			os.execute("cat satfile-START.cnf satfile-CLAUSES.cnf > satfile.cnf")
			os.execute("rm satfile-START.cnf")
			os.execute("rm satfile-CLAUSES.cnf")
		else
			error("function not implemented for your system!")
		end
	end
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)
		if type(v)=="number" then
			print(s..": ".." unknown")
		elseif type(v)=="boolean" then
			print(s..": "..tostring(v))
		elseif type(v)=="table" then
			for key, val in pairs(v) do
				PrintVar(s.."["..key.."]", val)
			end
		end
	end
	for key, val in pairs(Sol) do
		PrintVar(key, val)
	end
end

NewVar("always_true")
NewVar("always_false")
AddSimpleClause{Var.always_false, false}
AddSimpleClause{Var.always_true, true}

-- format: a1,1 a1,2 a1,3 a2,1 a2,2 a2,3 a3,1 ... an,3
-- result: whenever am,1 is true, am2, am,3 will appear in the final clause
function ConditionalClause(ccl)
	local cl = {}
	for i = 1, #t, 3 do
		assert(type(t[i]) == "boolean", "Position "..i.." is not boolean, it is "..type(t[i]).."!")
		assert(type(t[i+1]) == "number", "Position "..(i+1).." is not number, it is "..type(t[i+1]).."!")
		assert(type(t[i+2]) == "boolean", "Position "..(i+2).." is not boolean, it is "..type(t[i+2]).."!")

		if t[i] then
			cl[#cl+1] = t[i+1]
			cl[#cl+1] = t[i+2]
		end
	end
	return cl
end