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

Question

我想知道Java解算器API是如何解决其伪布尔问题的。我浏览过javadoc，但我对SAT问题还是个新手。

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

有谁有具体的知识吗？

Answer 1

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