java 降低可满足性的算法
有没有什么算法可以减少卫星问题。
可满足性是确定给定布尔公式的变量是否可以以使得公式计算为 TRUE 的方式分配的问题。同样重要的是确定是否不存在这样的赋值，这意味着公式表达的函数对于所有可能的变量赋值都是相同的 FALSE。在后一种情况下，我们会说该函数是不可满足的；否则是可以满足的。为了强调这个问题的二元性质，它经常被称为布尔或命题可满足性。简写“SAT”也常用来表示它，隐含的理解是该函数及其变量都是二进制值。
我已经使用遗传算法来解决这个问题，但如果减少它会更容易第一的？。
Is there any algorithm to reduce sat problem.
Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. The shorthand "SAT" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued.
I have used genetic algorithms to solve this, but it would be easier if is reduced first?.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
查看降阶二元决策图 (ROBDD)。它提供了一种将布尔表达式压缩为简化规范形式的方法。有很多软件可以执行 BDD 缩减，上面的 ROBDD 维基百科链接在文章底部包含了指向其他相关包的外部链接的很好列表。
Take a look at Reduced Order Binary Decision Diagrams (ROBDD). It provides a way of compressing boolean expressions to a reduced canonical form. There's plenty of software around for performing the BDD reduction, the wikipedia link above for ROBDD contains a nice list of external links to other relevant packages at the bottom of the article.
您可能可以对公式进行深度优先路径树搜索来识别“路径” - 即，对于 (ICanEat && (IHaveSandwich || IHaveBanana))，如果“ICanEat”为 false，则括号中的值不会没关系，可以忽略。因此，您可以在那里丢弃一些边和节点。
而且，如果在生成此深度优先搜索时，当前 Node 解析为 True，则您已经找到了解决方案。
You could probably do a depth-first path-tree search on the formula to identify "paths" - Ie, for (ICanEat && (IHaveSandwich || IHaveBanana)), if "ICanEat" is false, the values in brackets don't matter and can be ignored. So, right there you can discard some edges and nodes.
And, if while you're generating this depth-first search, the current Node resolves to True, you've found your solution.
你所说的“减少”到底是什么意思？我假设您的意思是事先进行某种预处理，可能首先消除或简化一些变量或子句。
这完全取决于您想要做多少工作。当然，您应该单元传播直到完成。您还可以做其他更昂贵的事情。有关一些示例，请参阅 march_dl 页面的预处理部分。
What do you mean by "reduced", exactly? I'm going to assume you mean some sort of preprocessing beforehand, to maybe eliminate or simplify some variables or clauses first.
It all depends on how much work you want to do. Certainly you should do unit propagation until it completes. There are other, more expensive things you can do. See the pre-processing section of the march_dl page for some examples.