Given my logical questions have options {True, False, Unknown}, Is is possible for me to use Z3 to solve it? I am hoping to learn more about Z3 and its potential of using it as a theorum solver (P.S. I know Prolog and Pyke might be more suitable for this task, but I find Z3 very easy to use.) I am using the solver.check() method and Z3 has been able to solve the questions perfectly. My question is whether Z3 is able to distinguish between False and Unknown? If yes, how do I do it? If No, why?
As example, the answer to this question is unknown.
# Charlie is green.
green(charlie)
# Charlie is kind.
kind(charlie)
# Charlie is nice.
nice(charlie)
# Charlie is rough.
rough(charlie)
# Erin is kind.
kind(erin)
# Erin is nice.
nice(erin)
# Erin is quiet.
quiet(erin)
# Fiona is quiet.
quiet(fiona)
# Fiona is rough.
rough(fiona)
# Harry is smart.
smart(harry)
# All rough, green people are quiet.
ForAll([x], Implies(And(rough(x), green(x)), quiet(x)))
# If someone is green and rough then they are nice.
ForAll([x], Implies(And(green(x), rough(x)), nice(x)))
# All kind, smart people are green.
ForAll([x], Implies(And(kind(x), smart(x)), green(x)))
# If Erin is green and Erin is blue then Erin is quiet.
ForAll([x], Implies(And(green(erin), blue(erin)), quiet(erin)))
# All quiet people are smart.
ForAll([x], Implies(quiet(x), smart(x)))
# All kind people are green.
ForAll([x], Implies(kind(x), green(x)))
# If someone is smart then they are kind.
ForAll([x], Implies(smart(x), kind(x)))
# All rough, nice people are blue.
ForAll([x], Implies(And(rough(x), nice(x)), blue(x)))
# Question: The statement "Based on the above information, is the following statement true, false, or unknown? Erin is rough" is True ,False or Unknown?
return rough(erin)
I have tried to solve it this way,
from z3 import *
ThingsSort, (charlie, erin, fiona, harry) = EnumSort('ThingsSort', ['charlie', 'erin', 'fiona', 'harry'])
green = Function('green', ThingsSort, BoolSort())
kind = Function('kind', ThingsSort, BoolSort())
blue = Function('blue', ThingsSort, BoolSort())
smart = Function('smart', ThingsSort, BoolSort())
rough = Function('rough', ThingsSort, BoolSort())
quiet = Function('quiet', ThingsSort, BoolSort())
nice = Function('nice', ThingsSort, BoolSort())
x = Const('x', ThingsSort)
precond = []
precond.append(green(charlie))
precond.append(kind(charlie))
precond.append(nice(charlie))
precond.append(rough(charlie))
precond.append(kind(erin))
precond.append(nice(erin))
precond.append(quiet(erin))
precond.append(quiet(fiona))
precond.append(rough(fiona))
precond.append(smart(harry))
precond.append(ForAll([x], Implies(And(rough(x), green(x)), quiet(x))))
precond.append(ForAll([x], Implies(And(green(x), rough(x)), nice(x))))
precond.append(ForAll([x], Implies(And(kind(x), smart(x)), green(x))))
precond.append(ForAll([x], Implies(And(green(erin), blue(erin)), quiet(erin))))
precond.append(ForAll([x], Implies(quiet(x), smart(x))))
precond.append(ForAll([x], Implies(kind(x), green(x))))
precond.append(ForAll([x], Implies(smart(x), kind(x))))
precond.append(ForAll([x], Implies(And(rough(x), nice(x)), blue(x))))
s = Solver()
s.add(precond)
s.add(Not(rough(erin)))
if s.check() == unsat:
print('True')
elif s.check() == sat:
print('False')
else:
print('Unknown')
But the output of this question is false.
Just to set the terminology: When an SMT solver says sat, it means that the asserted facts are all consistent together. When it says unsat, it means that there is no assignment to variables that makes all the assertions true. When it says unknown, it means the analysis was incomplete and it couldn't decide. This final case can happen if the problem is not in the decidable fragment of the supported logic, or if a timeout happens, or some other exception occurs.
Your use of "Unknown," however is different: It's not what an SMT solver means by unknown. You use "Unknown" to mean "does this necessarily follow." So, the two uses are, confusingly perhaps, are different.
Based on this, what you want to do is to ask the solver if there is a way to satisfy rough(erin), and also Not(rough(erin)). If both are satisfiable, then you cannot deduce, i.e., it would be your "Unknown" case. If only one of them is satisfiable and the other isn't, then you know what logically follows. You can use the incremental interface to z3 to achieve this, as follows:
from z3 import *
ThingsSort, (charlie, erin, fiona, harry) = EnumSort('ThingsSort', ['charlie', 'erin', 'fiona', 'harry'])
green = Function('green', ThingsSort, BoolSort())
kind = Function('kind', ThingsSort, BoolSort())
blue = Function('blue', ThingsSort, BoolSort())
smart = Function('smart', ThingsSort, BoolSort())
rough = Function('rough', ThingsSort, BoolSort())
quiet = Function('quiet', ThingsSort, BoolSort())
nice = Function('nice', ThingsSort, BoolSort())
x = Const('x', ThingsSort)
s = Solver()
s.add(green(charlie))
s.add(kind(charlie))
s.add(nice(charlie))
s.add(rough(charlie))
s.add(kind(erin))
s.add(nice(erin))
s.add(quiet(erin))
s.add(quiet(fiona))
s.add(rough(fiona))
s.add(smart(harry))
s.add(ForAll([x], Implies(And(rough(x), green(x)), quiet(x))))
s.add(ForAll([x], Implies(And(green(x), rough(x)), nice(x))))
s.add(ForAll([x], Implies(And(kind(x), smart(x)), green(x))))
s.add(ForAll([x], Implies(And(green(erin), blue(erin)), quiet(erin))))
s.add(ForAll([x], Implies(quiet(x), smart(x))))
s.add(ForAll([x], Implies(kind(x), green(x))))
s.add(ForAll([x], Implies(smart(x), kind(x))))
s.add(ForAll([x], Implies(And(rough(x), nice(x)), blue(x))))
# Is the predicate consistent with the existing facts
# in the solver?
def isConsistent(solver, predicate):
solver.push()
solver.add(predicate)
r = solver.check()
solver.pop()
if r == sat:
return True
elif r == unsat:
return False
else:
raise SolverInconclusive
erinCanBeRough = isConsistent(s, rough(erin))
erinCanBeNotRough = isConsistent(s, Not(rough(erin)))
if erinCanBeRough and erinCanBeNotRough:
print("Unknown")
elif erinCanBeRough:
print("Erin is rough")
elif erinCanBeNotRough:
print("Erin is not rough")
else:
print("The existing facts are inconsistent already.")
When I run this, I get:
Unknown
as you were expecting. Note the call to push/pop to manage the assertion stack so we don't pollute the "fact base" when we want to see if the predicate we're checking (and its negation) is satisfiable. This is managed by the isConsistent function. Also note how we raise an error if the solver returns anything other than sat or unsat (which will be unknown essentially but in the SMT-solver sense as I explained above, not in your sense), as in this case we cannot conclude anything.