我有以下问题:
我有两个必须在逻辑上等价的命题公式。只有其中一个包含了变量，也就是说，变量可以被任何命题公式所代替。现在的问题是，我需要找到这个变量的实际替代物，这样逻辑等价就成立了。例子:
(a ^ ~b)或x = a
这里，x表示变量。这个逻辑等价可以通过用a ^ b替换x来实现，所以它变成:
(a ^ ~b)或(a ^ b) = a
这就是问题所在。我需要一个算法，输入"一个变量x的方程"，并给出变量x的输出值，使方程成为逻辑等价。
总是有一个变量。(事实上，我可能会遇到多个变量的问题，但我想先解决简单的情况)。所讨论的公式可以有任何形式(它们不是CNF或DNF)。此外，公式实际上可以是FALSE或TRUE，并且在没有解的情况下(例如，对于"a或x = FALSE "，没有解)或有多个解的情况下(例如，对于"a和x = FALSE "，任何假命题都是有效答案)。
我只有一个表推理器，它告诉我一个公式是否可满足。所以我可以测试一个解决方案。但我的问题是给我一个解决方案。
我相信您正在寻找的是一个可以处理未解释函数的推理引擎。这样的引擎可以处理包含函数的问题，例如
(a ^ ~b)或f(a,b) = a
，它们通常能够生成模型，也就是说，它们实际上会生成满足初始公式的函数f(…)。合适的推理引擎的一个例子是所谓的SMT求解器(参见SMT- lib)。一个流行的求解器是微软的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为有限域(如布尔域)上的量词使用了一个完整的推理引擎，并且能够为这些公式生成模型。