3-SAT公式作为SMT-LIB

Question

我试图找出这种A的值是否能使布尔表达式成为真。我使用在线z3解算器(https://jfmc.github.io/z3-play/)，它会产生错误

错误：(错误“第11行，第12列:传递给函数的参数数(4)错误”)

这是我的密码：

(set-logic QF_LIA)
(declare-const A Bool)
(declare-const B Bool)
(declare-const C Bool)
(declare-const D Bool)
(declare-const E Bool)
(declare-const F Bool)
(assert
(and
(A or B or C)
(D or E or F)
))
(check-sat)
(get-model)
(exit)

Answer 1

在SMTLib中，函数是用前缀表示法编写的.因此，与其：

(assert
(and
(A or B or C)
(D or E or F)
))

你应该使用：

(assert (and (or A B C)
             (or D E F)
        )
)

这类似于Lisp/Scheme这样的语言，其中前缀表示法使得语法更容易被程序解析/操作。