特别是,它是否使用DPLL(T)？它是否使用低于/高于近似值？它是否在单词级别处理线性算术？那么非线性算术呢？
我在文章中只发表了一篇关于"类似于MathSAT/Boolector中的简化"的表面提及,以便有效地解决量化比特公式.
非常有趣的是什么方法帮助Z3在smtcomp的QF_BV部分获得第一名.
DPLL(T)根本不用于解决QF_BV问题.关于"有效地解决量化比特公式"的论文的评论是关于Z3 2.x. QF_BV是关于问题编码的.预处理有很大的不同.我为Z3 3.0从零开始构建了一个新的预处理堆栈和SAT求解器.新的预处理器比Z3 2.x中使用的预处理器快得多,并且执行更积极的简化.没有神奇或奇特的技巧.在预处理步骤之后,Z3对所有内容进行bit-blast并调用新的SAT求解器.Z3不使用欠/近似的位向量,或字级算术推理,或对非线性算子的特殊支持.顺便说一下,很少有解决方案考虑的一点是,一些简化可能会减少本地公式的大小,但会全局增加,因为它们会破坏共享.Z3还使用预处理步骤,试图增加线性和非线性位向量算法中的共享量.