2

我有以下问题：

我有两个必须成为逻辑等价的命题公式。只有其中一个包含一个“变量”，因为该变量可以被任何命题公式替换。现在的问题是，我需要找到变量的实际替换，以便逻辑等价变为真。例子：

(a ^ ~b) 或 x = a

这里，x 表示变量。通过将 x 替换为 a ^ b 可以使这个逻辑等价成立，因此它变为：

(a ^ ~b) 或 (a ^ b) = a

所以这就是问题所在。我需要一种算法，该算法将“具有一个变量 x 的方程”作为输入，并给出变量 x 的输出值，以使方程成为逻辑等价。

永远只有一个变量。（实际上我可能会遇到多个变量的问题，但我想先解决简单的情况）。有问题的公式可以有任何形式（它们不在 CNF 或 DNF 中）。此外，公式实际上可以为 FALSE 或 TRUE，并且在某些情况下，没有解决方案（例如，对于“a 或 x = false”，没有解决方案）或多个解决方案（例如，对于“a and x = false”） “任何错误的命题都是有效的答案）。

我所拥有的只是一个画面推理器，它告诉我一个公式是否可以满足。所以我可以测试一个解决方案。但我的问题是给我一个解决方案。

4

1 回答 1

1

我相信您正在寻找的是可以处理未解释功能的推理引擎。这样的引擎可以处理包含函数的问题，例如，

(a ^ ~b) 或 f(a,b) = a

他们通常能够生成模型，也就是说，它们实际上会生成一个满足您的初始公式的函数 f(...)。合适的推理引擎的一个例子是所谓的 SMT 求解器（参见SMT-LIB）。一个流行的求解器是 Microsoft 的 Z3（参见Z3）。

该示例可以用 SMT-LIB 格式表述如下：

(set-option :produce-models true)
(declare-const a Bool)
(declare-const b Bool)
(declare-fun f (Bool Bool) Bool)

(assert (= (or (xor a (not b)) (f a b)) a))
(check-sat)
(get-model)
(exit)

Z3 生成模型

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool 
  (ite (and (= x!1 false) (= x!2 true)) false false))

这满足了原始问题。一般来说，解决方案只满足问题。为了获得完整的解决方案，可以使用量词。并非所有 SMT 求解器都支持它们，但例如 Z3 使用完整的推理引擎来处理有限域上的量词（如布尔值），并且能够为此类公式生成模型。

于 2011-10-12T21:41:46.670 回答