使用 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 求解器求解的主要内容,如果未能解决你的问题,请参考以下文章