带True/False/Unknown选项的逻辑问题能否用Z3求解？如何区分二者？

需求说明 #

需要用Z3定理求解器处理逻辑推理问题，判断命题属于True（必然成立）、False（必然不成立）还是Unknown（无法确定）。虽已知Prolog、Pyke更适配这类任务，但因Z3易用性优先选择它，当前代码无法正确区分False和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)))

# 问题："Erin is rough" 是True、False还是Unknown？

用户错误实现代码 #

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')

该代码输出False，但正确答案应为Unknown。

错误原因分析 #

当前代码仅检查了「Erin不是rough」是否与前提兼容，若兼容就输出False，但这忽略了「Erin是rough」也可能与前提兼容的情况——当两种情况都兼容时，命题应为Unknown。

正确解决方案 #

需要同时检查原命题和其否定与前提的兼容性，修改后的代码如下：

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_true = Solver()
s_true.add(precond)
s_true.add(Not(rough(erin)))  # 检查原命题的否定是否不可满足

s_false = Solver()
s_false.add(precond)
s_false.add(rough(erin))  # 检查原命题是否不可满足

check_true = s_true.check()
check_false = s_false.check()

if check_true == unsat:
    print('True')  # 原命题否定不成立 → 原命题必然为真
elif check_false == unsat:
    print('False')  # 原命题本身不成立 → 原命题必然为假
else:
    print('Unknown')  # 两种情况都成立 → 无法确定

运行后输出Unknown，符合预期。

原理说明 #

Z3的solver.check()返回值对应逻辑兼容性：

• sat：当前约束与前提兼容（存在至少一种模型满足）
• unsat：当前约束与前提矛盾（无任何模型满足）
• unknown：Z3无法判定兼容性（通常因问题复杂度太高）

对应到三值逻辑推理：

1. 若原命题的否定与前提矛盾（s_true.check() == unsat）→ 原命题必然为True
2. 若原命题本身与前提矛盾（s_false.check() == unsat）→ 原命题必然为False
3. 若原命题和其否定都与前提兼容 → 原命题为Unknown（两种情况都可能成立，无法确定）

内容的提问来源于stack exchange，提问作者Matthew Lam