Commit 19d1e169 authored by Karel Koci's avatar Karel Koci 🤘

picosat: allow max_satisfiable for satisfiable result

Function max_satisfiable can be called even if result is satisfiable.
In such case it returns all assumptions. But less handy is that it
reassumes all assumptions. This is now noted in documentation and some
tests were added for this purpose.
parent efef32e2
......@@ -220,8 +220,9 @@ It returns object with following methods:
satisfiable():: Checks if clauses are satisfiable with given
assumptions. Returns true or false accordingly.
max_satisfiable():: Generates maximal satisfiable subset of assumptions.
Can be called only after `satisfiable` returned false. Returns set
of all assumptions that can be assumed at the same time.
Can be called only after `satisfiable`. Returns set of all assumptions
that can be assumed at the same time. Note that this reassumes previous
assumptions, so they are again valid for next `satisfiable` call.
After calling `satisfiable` you can access assigned values by indexing
object with variable you are interested in. It returns true or false.
......
......@@ -92,10 +92,12 @@ static int lua_picosat_satisfiable(lua_State *L) {
static int lua_picosat_max_satisfiable(lua_State *L) {
struct picosat *ps = luaL_checkudata(L, 1, PICOSAT_META);
ASSERT_MSG(picosat_res(ps->sat) == PICOSAT_UNSATISFIABLE, "picosat:satisfiable can be called only when picosat:satisfiable returns false.");
lua_newtable(L);
if (picosat_inconsistent(ps->sat))
// If there is some empty clause, then there are no valid assumptions, return empty table.
return 1;
// TODO this might be faster if we would set phase for assumptions to true. See picosat documentation for more details.
const int *assum = picosat_maximal_satisfiable_subset_of_assumptions(ps->sat);
lua_newtable(L);
while(*assum != 0) {
lua_pushinteger(L, *assum);
lua_pushboolean(L, true);
......
......@@ -80,6 +80,9 @@ function test_assume()
assert_false(ps:satisfiable())
ps:assume(-var2)
assert_true(ps:satisfiable())
ps:assume(var3)
ps:assume(-var1)
assert_true(ps:satisfiable())
end
function test_max_satisfiable()
......@@ -98,4 +101,18 @@ function test_max_satisfiable()
assert_true((not maxassum[var2] and maxassum[var3] == nil) or (maxassum[var2] == nil and maxassum[var3]))
-- and souldn't contain var1
assert_nil(maxassum[var1])
-- Drop reassumed assumptions
assert_false(ps:satisfiable())
-- Check if we get all assumptions even when it is satisfiable
ps:assume(-var1)
ps:assume(var2)
ps:assume(var3)
assert_true(ps:satisfiable())
local maxassum = ps:max_satisfiable()
assert_true(maxassum[-var1])
assert_true(maxassum[var2])
assert_true(maxassum[var3])
-- Drop reassumed assumptions
assert_true(ps:satisfiable())
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment