在不重复布尔表达式的情况下使用 Z3 解决 SAT 问题

Question

我们来看下面的问题：f(a, b, c, x, y, z)是一个布尔函数，其中a、b、c、x、y和z是布尔值，f的输出是一个布尔值。 f 的定义由许多 and/or/nor 运算符组成。我想找到一组三个布尔值 x0、y0 和 z0，这样：

f(0, 0, 0, x0, y0, z0) = 0 AND
f(0, 0, 1, x0, y0, z0) = 1 AND
f(0, 1, 0, x0, y0, z0) = 1 AND
f(0, 1, 1, x0, y0, z0) = 0 AND
...
f(1, 1, 1, x0, y0, z0) = 1 # A total of 8 constrains. Each of them is from an entry in the truth table.

一种天真的做法是定义3个布尔变量x、y、z，重复定义函数f8次。然而 f 由复杂的布尔表达式组成。定义它 8 次可以炸毁模型。而且，实际上，我有 7 个变量：a、b、c、d、e、f、g。真值表有 128 个条目。

有没有办法定义诸如“占位符”变量 a、b、c 之类的东西，它们不是解决方案的一部分？然后我可以在 a、b、c、x、y、z 上只定义一次 f，然后以某种方式将 a、b、c “分配”给布尔常量。

我是 SMT 求解器的新手，占位符的想法可能完全无关紧要。其他解决方案也值得赞赏。

Answer 1

我不清楚你需要模型做什么以及需要多大的灵活性，但这里有一个想法：如果可以通过单个 else-case 将函数约束在所有参数值上，那么以下可能工作：

(declare-fun f (Bool Bool Bool Bool) Bool)

(assert (forall ((x Bool) (y Bool) (z Bool) (p Bool)) (!
  (=
    (f x y z p)
    (ite
      (and (not x) y) true (ite         ; 1. case
      (and (not x) (not y) z) true (ite ; 2. case
      (and x (not y) z) true            ; 3. case
      false))))                         ; else-case
  :pattern ((f x y z p)))))

至少对于这个简单的案例，Z3 的模型有效地忽略了函数f 无关的第四个参数：

(check-sat) ;; SAT --> good
(get-model)  
; NOTE: 4th parameter x!3 is declared, but not used
; (model 
;   (define-fun p () Bool
;     false)
;   (define-fun f ((x!0 Bool) (x!1 Bool) (x!2 Bool) (x!3 Bool)) Bool
;     (or (not (or x!0 (not x!1)))
;         (not (or x!1 (not x!2) (not x!0)))
;         (not (or x!1 x!0 (not x!2)))))
; )

Answer 2

很难准确地理解你想要做什么。但在我看来，您关心的是如何轻松编写代码，而不是其他任何事情。如果是这样，我建议使用提供比 SMTLib 更高级别 API 的语言进行编程。您可以使用 z3 支持的许多接口：C、C++、Java 等，以简化编程任务。

例如，以下是使用 Python 接口编写问题实例的方法：

from z3 import *

def fOriginal(a, b, c, x, y, z):
    return Or([a, b^c, x, y, z])

x0, y0, z0 = Bools("x0 y0 z0")

def f(a, b, c):
    return fOriginal(a == 1, b == 1, c == 1, x0, y0, z0)

s = Solver()

s.add(f(0, 0, 0) == False)
s.add(f(0, 0, 1) == True)
s.add(f(0, 1, 0) == True)
s.add(f(0, 1, 1) == False)
s.add(f(1, 1, 1) == True)

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

运行时，会打印：

sat
[y0 = False, z0 = False, x0 = False]

给你分配x0、y0 和z0 的任务。

这里的想法是将f 编码为常规函数，使用z3 的接口。我在 python 代码中调用了这个函数fOriginal。然后我们定义了fOriginal 的一个版本，我在代码中将其称为f，它为最后三个参数传递符号值，但期望前三个参数为常量。

然后，我们只需为您的每个案例添加约束条件。按照您的示例，我仅在上面添加了 5 个；当然，你可以添加所有 8 个。

我希望这能让你开始！