降低可满足性的算法java答案

【问题标题】：Algorithm to reduce satisfiability java降低可满足性的算法java
【发布时间】：2011-03-14 00:43:20
【问题描述】：

有什么算法可以减少sat问题。

可满足性是确定给定布尔公式的变量是否可以以使公式评估为 TRUE 的方式分配的问题。同样重要的是确定是否不存在这样的赋值，这意味着公式表示的函数对于所有可能的变量赋值都是相同的 FALSE。在后一种情况下，我们会说函数是不可满足的；否则是可以满足的。为了强调这个问题的二元性质，它经常被称为布尔或命题可满足性。简写“SAT”也常用来表示它，隐含的理解是函数及其变量都是二进制值。

我已经使用遗传算法解决了这个问题，但是如果先减少它会更容易吗？。

【问题讨论】：

标签： java algorithm performance genetic-algorithm

【解决方案1】：

看看Reduced Order Binary Decision Diagrams (ROBDD)。它提供了一种将布尔表达式压缩为简化规范形式的方法。有很多用于执行 BDD 减少的软件，上面的 ROBDD 维基百科链接包含一个很好的外部链接列表，指向文章底部的其他相关包。

【讨论】：

【解决方案2】：

您可以对公式进行深度优先路径树搜索以识别“路径”-即，对于 (ICanEat && (IHaveSandwich || IHaveBanana))，如果“ICanEat”为假，则括号中的值不会没关系，可以忽略。所以，你可以在那里丢弃一些边和节点。

而且，如果在您生成此深度优先搜索时，当前节点解析为 True，那么您已经找到了解决方案。

【讨论】：

【解决方案3】：

你所说的“减少”到底是什么意思？我假设您的意思是事先进行某种预处理，以首先消除或简化一些变量或子句。

这完全取决于你想做多少工作。当然你应该做unit propagation直到它完成。您还可以做其他更昂贵的事情。有关示例，请参阅march_dl 页面的预处理部分。

【讨论】：