0

I wish to solve the following SAT-related problem, preferably using Z3 or some other freely available solver:

Given a set of formulae of predicate logic (without quantifiers or negation) over a set of Boolean variables, find the maximal subset of the variables, such that if true is assigned precisely to all variables in this subset, all the formulae are satisfied. The formulae are all of the form variable => CNF-formula.

Generally, I want to find an "optimal" solution to the classical SAT problem, which is the valuation assigning true to the most variables possible.

Борат Сагдиев
  • 127
  • 11

1 Answers1

2

General method

You can use the z3's optimize engine to solve this. Here's an example.

Let's say we have 4 variables a, b, c, d, and the predicates are a -> b&c and c & !d. We first create them and add the constraints to the engine:

from z3 import *

a, b, c, d = Bools('a b c d')
bools = [a, b, c, d]

s = Optimize()
s.add(Implies(a, And(b, c)))
s.add(And(c, Not(d)))

Now we keep a counter, and add 1 to it for each true variable:

goal = 0
for v in bools:
    goal = goal + If(v, 1, 0)

Finally, we tell z3 to maximize this goal:

s.maximize(goal)

We can now query for the optimal model:

print(s.check())
print(s.model())

This prints:

sat
[b = True, a = True, d = False, c = True]

from which we can conclude that a maximally satisfying subset is {a, b, c} for our constraints; which you can easily see is also the only one.

Using Soft Constraints

Another way to do this would be to add soft-constraints for each boolean instead of creating the goal variable, something like this:

from z3 import *

a, b, c, d = Bools('a b c d')

s = Optimize()
s.add(Implies(a, And(b, c)))
s.add(And(c, Not(d)))

s.add_soft(a)
s.add_soft(b)
s.add_soft(c)
s.add_soft(d)

print(s.check())
print(s.model())

This'll produce the exact same output; and is equivalent when all you want to do is maximize the number of true assignments. (The first form is more general if you want to prioritize certain variables over others, since you can assign different "integers" instead of 1 to all to insure they are preferable over others.)

alias
  • 28,120
  • 2
  • 23
  • 40
  • Excellent, thank you. BTW `goal = sum(If(v, 1, 0) for v in bools)` also seems to work. – Борат Сагдиев Apr 16 '21 at 17:02
  • And one more question – how to find _all_ optimal assignments? Is there a way to do it other than adding the clause `(!v1 or !v2 or !v3 ...)` after finding each model {v1, v2, v3...} ? – Борат Сагдиев Apr 16 '21 at 18:15
  • There's a couple of different ways to get "all-solutions." The basic idea is to iteratively add constraints to refute older models, till you get `unsat`. See this answer for details: https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation – alias Apr 16 '21 at 23:35