使用 DPLL sat 求解器求解

Posted

技术标签:

【中文标题】使用 DPLL sat 求解器求解【英文标题】:Solving using DPLL sat solver 【发布时间】:2011-04-29 07:51:35 【问题描述】:

我在

中找到了一个SAT求解器

http://code.google.com/p/aima-java/

我尝试了以下代码来使用 dpllsolver 解决表达式

输入是

(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))

CNF 转换器将其转换为

 (  (  ( NOT A )  OR B ) AND  (  ( NOT B )  OR A ) )

不考虑其他部分的逻辑,只考虑第一项,如何让它正常工作?

如果其他卫星求解器可以做到,请建议我

PEParser parser = new PEParser();
CNFTransformer transformer=new CNFTransformer();
Sentence and;
Sentence transformedAnd;
DPLL dpll = new DPLL();

Sentence sentence = (Sentence) parser.parse("(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))");
transformedAnd = transformer.transform(sentence);

System.out.println(transformedAnd.toString());
boolean satisfiable = dpll.dpllSatisfiable(transformedAnd);

System.out.println(satisfiable);

【问题讨论】:

【参考方案1】:

试试这个:http://www.sat4j.org/

我相信这项技术已被纳入 Eclipse Provisioning System P2 以解决插件依赖性。 http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology-for-managing-plugins

【讨论】:

以上是关于使用 DPLL sat 求解器求解的主要内容,如果未能解决你的问题,请参考以下文章

SAT DPLL CDCL

SAT DPLL CDCL

SAT求解器快速入门

Dafny 作为 SAT-QBF 求解器没有给出正确的结果

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

本人研究sat求解器数据信息汇总