java - SAT4J 如何解决伪布尔问题？它是使用自定义的伪布尔求解器还是将约束转换为 CNF？

Question

我想知道 Java SAT4j SAT 求解器 API 如何解决它的伪布尔问题。我浏览过 javadoc，但我对 SAT 问题还是很陌生。

从发布文档（https://www.researchgate.net/publication/220163278_The_Sat4j_library_release_22）中，我认为自定义的伪布尔求解器用于所有事情，而不是反之亦然（伪布尔约束转换为 SAT CNF）。

谁有具体的知识？

Answer 1

Sat4j 不翻译 CNF 中的基数或伪布尔约束，它使用分辨率证明系统或某种称为广义分辨率的“切割平面”证明系统本地处理它们。