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

Posted 2021-04-02

我想知道Java SAT4j SAT求解器API如何解决其伪布尔问题。我已经浏览了javadoc，但我对SAT问题很新。

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

谁有具体的知识？

答案

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