Can Z3 answer that question?

[14H034160212]

Hi,

I am trying to use SAT Solver to answer the following question. The context is given by (¬α->¬β,¬β->¬γ). For each option, there are ( ¬ γ -> ¬ α ), ( γ -> α ), ( ¬ γ -> ¬ β ), and ( α -> γ ). Option B can be selected using contraposition law and transitive law. Can Z3 select the correct answer by given the context? If yes, how to do that? If not, is there any other SAT solver can do that? Many thanks.

[aytey]

I think it seems quite unclear what you're trying to; do you want Z3 to tell you the possible options out of the context?

If so, it seems that you want to assert ¬a -> ¬b and ¬b -> ¬c and then use Z3 to find all solutions to model (which can be done using https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations)

[14H034160212]

I see. You got the point. So, I guess SAT Solver cannot only select option B as the correct option by giving these context rules? Cause even I set all variables as True, I can also derive other options as True, not only option B is correct.

[aytey]

The solver here (which may or may not be a SAT solver, depending on your formula) is welcome to make any assignment, meeting the assertions you add. If you don't want "other options" then you need to add a clause that says "and not this".

[14H034160212]

OK. I thought the SAT solver could automatically find those other options that cannot be derived from the context rules.

[14H034160212]

I write the context rules and optionB in the following way, but the return result is an empty list.
((not a -> not b) and (not b -> not c)) -> (c -> a)

What is the meaning of the empty list? Cause I also try another simple example. I also got an empty list.
(a->b and b->c) -> (a->c)

If there is no solution, the console will print no solution like that. So, maybe empty list [] means a different meaning?

[14H034160212]

I finally understand that the specific use here can be changed to the rule in the given context as a condition, each option is used as a conclusion, and the condition is used to derive the opposite of the conclusion, which shows that the opposite of the conclusion is unsatisfiable, so the conclusion is true. I tried it with this method, and it’s okay. Now only the opposite of optionB is unsat, and the others are sat. It can be seen that only optionB is correct.
The negation of Option A: ((not a -> not b) and (not b -> not c)) -> not ( not c -> not a)
The negation of Option B: ((not a -> not b) and (not b -> not c)) -> not (c -> a)
The negation of Option C: ((not a -> not b) and (not b -> not c)) -> not ( not c -> not b)
The negation of Option D: ((not a -> not b) and (not b -> not c)) -> not ( a -> c)
And then only the negation of option B return unsat and the others all return sat . So I can ensure that option B is definitely true.

from z3 import *
a = Bool('a')
b = Bool('b')
c = Bool('c')
s = Solver()

s.add(Or(a, (Not(b))))
s.add(Or(b, (Not(c))))
print("case a")
s.push()
s.add(Not(Or(c,Not(a))))
print(s.check())
s.pop()

print("case b")
s.push()
s.add(Not(Or(Not(c),a)))
print(s.check())
s.pop()

print("case c")
s.push()
s.add(Not(Or(c,Not(b))))
print(s.check())
s.pop()

print("case d")
s.push()
s.add(Not(Or(Not(a),c)))
print(s.check())
s.pop()