【发布时间】：2014-06-15 05:53:35
【问题描述】：
DNF SAT 是多项式时间，而 CNF SAT 是 NP-Complete。如果我有一个布尔骨架已经在 DNF 中的一阶公式，z3 会意识到这一点，还是会盲目地将公式转换为 CNF 以通过 CDCL 求解？
【问题讨论】：
【发布时间】：2014-06-15 05:53:35
【问题描述】：
它可能，尤其是在具有推/拉和/或 API 中使用的策略的交互式上下文中。发生这种情况时，产生的约束应该相对容易解决。然而，这确实引出了一个问题，为什么所有的立方体都被交给 Z3，当它们中的每一个都可以被独立检查时，留下更少的空间让启发式混淆。
【讨论】：
-
谢谢。这意味着逐个迭代检查每个杯子比检查所有杯子的分离更有效。我说的对吗？
-
可能，是的。这实际上取决于每个文字中的确切内容。例如，当所有析取项共享一个简化器可以简化的理论表达式并且使所有析取项为假时，同时对所有析取项运行 Z3 会更快，以避免重复调用简化器。相反，如果每个 discjuncts 都完全描述了一个不同的模型，那么将它们全部编码只是为了选择第一个作为结果将是不必要的开销。