问题标签 [dpll]

I'm doing a SAT Solver (mainly the DPLL or Partial DPLL) and I have the method for Unit Propogation. Basically what it does is that it checks whether there are any standalone literals, and removes that literal, and any instance found in the other clauses. Any Example would be

the Unit Propogation would be 'x' and when performing the unit prop it would leave only (w,z)

In this method I have several nested foreach loops and List<literals> <literals> is a custom made class which has 2 variables hasNegation (bool) and char literalCharacter

The Coding is below, and will explain from below

I have 2 List <literals> which are templist and listOfLiterals where the LATTER is the "parent"

I am tryign to remove the entries of listOfLiterals that match with tempList and I use c2.listOfLiterals.RemoveAll(tempList); obviously will output an error as it is not a Delegate.

I've searched a lot,even on stackoverflow, but every one of them compares either to an ID or an integer. In my case, since I'm just comparing 2 Lists, how can I do the delegate so that, the entries that are the same in both listOfLiterals and tempList are removed from listOfLiterals?

Many thanks

EDIT:

Literals Class

我想在 Prolog 中使用 DCG 解析逻辑表达式。

逻辑术语表示为列表，例如['x','&&','y']，x ∧ y结果应该是解析树and(X,Y)（过去X和Y现在都是未分配的 Prolog 变量）。

我实现了它，一切都按预期工作，但我有一个问题：
我无法弄清楚如何解析变量'x'并'y'获取真正的 Prolog 变量X以及Y以后分配真值。

我尝试了以下规则变体：

• v(X) --> [X].:
  这当然行不通，它只会返回and('x','y').
  但是我可以用 Prolog 变量统一替换这个术语中的逻辑变量吗？我知道谓词term_to_atom（它被提议作为类似问题的解决方案），但我认为它不能在这里使用来达到预期的结果。

• v(Y) --> [X], {nonvar(Y)}.：
  这确实会返回一个未绑定的变量，但当然每次都会返回一个新变量，即使逻辑变量（'x'，'y'，...）已经在术语中，所以 ['X','&&','X']被评估and(X,Y)为不是所需的结果，要么.

这个问题有什么优雅或惯用的解决方案吗？

提前谢谢了！

编辑：

这个问题的背景是我正在尝试在 Prolog中实现DPLL 算法。我认为将逻辑术语直接解析为 Prolog 术语以方便使用 Prolog 回溯工具会很聪明：

• 输入：一些逻辑项，例如 T =[x,'&&',y]
• 解析后的术语：（[G_123,'&&',G_456]现在具有“真实”的 Prolog 变量）
• 将 { boolean(t), boolean(f) } 中的值赋给 T 中的第一个未绑定变量。
• 简化术语。
• ...重复或回溯，直到v找到分配，v(T) = t或者搜索空间被耗尽。

我对 Prolog 很陌生，老实说，我想不出更好的方法。我对更好的选择非常感兴趣！（所以我有点半信半疑，这就是我想要的 ;-) 非常感谢你到目前为止的支持......）

这是一个非常简单的cnf实例，如(x1 or x2 or x3)&(x1 or x2)&(x2 or x3)，公式绝对可以满足，解x1 = x2 = x3 = 1，就够了。那么，我的问题是求解器如何使用 DPLL 或其他程序生成分配？谢谢。

我想在 Haskell 中实现上面的 DPLL 算法。但问题是我不知道如何运行多个 if 语句。所以我在想，你可以对前 2 个 if 语句进行模式匹配。但你不能为第三和第四？因为它们都必须运行，return 语句也必须运行。

如何在 Haskell 中创建多个类似上述的 if 语句？此外，我对 Haskell 还是很陌生，所以我无法做任何“复杂”的事情。

我想构建一个 SMT 公式，该公式具有对整数线性算术和布尔变量的许多断言，以及对实数非线性算术和布尔变量的一些断言。整数和实数的断言只共享布尔变量。例如，考虑以下公式：

如果我用这个公式喂 z3，它会立即报告“未知”。但是如果我删除它的整数部分，我会立即得到解决方案，它满足变量“r”的约束。我认为这意味着非线性约束本身对求解器来说并不难。问题应该在于对整数的（线性）约束和对实数的（非线性）约束的混合。

所以我的问题如下。使用 z3（如果有的话）处理这种混合公式的正确方法是什么？我对 DPLL(T) 的理解是，它应该能够使用针对不同约束的不同理论求解器来处理此类公式。如果我错了，请纠正我。

我正在尝试找到 Z3 的 c++ 文件，如果在当前分支上找不到解决方案，算法会在该文件中回溯。我一直在查看所有文件并在 python 文件上尝试了调试模式，但到目前为止还没有运气。我只想在方法中添加一个打印语句，这样我就可以知道它何时返回到前一个节点并尝试新路径。

谢谢！

I'm implementing DPLL algorithm that counts the number of visited nodes. I managed to implement DPLL that doesn't count visited nodes but I can't think of any solutions to the problem of counting. The main problem is that as the algorithm finds satisfying valuation and returns True, the recursion rolls up and returns counter from the moment the recursion started. In any imperative language I would just use global variable and increment it as soon as function is invoked, but it is not the case in Haskell.

The code I pasted here does not represent my attempts to solve the counting problem, it is just my solution without it. I tried to use tuples such as (True,Int) but it will always return integer value from the moment the recursion started.

This is my implementation where (Node -> Variable) is a heuristic function, Sentence is list of clauses in CNF to be satisfied, [Variable] is a list of Literals not assigned and Model is just a truth valuation.

I would really appreciate any advice on how to count the visited nodes. Thank you.

EDIT:

The only libraries I'm allowed to use are System.Random, Data.Maybe and Data.List.

EDIT:

One possible solution I tried to implement is to use a tuple (Bool,Int) as a return value from DPPL function. The code looks like:

The basic idea of this approach is to increment the counter at each recursive call. However, the problem with this approach is that I have no idea how to retrieve counter from recursive calls in OR statement. I'm not even sure if this is possible in Haskell.

我试图在实际编码之前了解 DPLL 程序。

例如，我有这些条款：

现在我将决策变量设为 d = 0, b = 0。子句现在看起来像这样。

单元传播和纯文字规则如何在这里发挥作用？

此外，在C3 : {1, !a}- 当我服用 时a = 1，这变成了{1, 0}。该子句的最终值应该是多少？应该是{1}吗？

如果任何子句具有 value {!b}，即对文字的否定，在应用决策变量之后，那么如何进行？

我正在编写一个 SAT 求解器，并开始实施 DPLL 算法。我了解该算法及其工作原理，我还实现了它的一个变体，但困扰我的是接下来的事情。

这是什么意思，这Φ是一组一致的文字？我理解不一致意味着假，这意味着一致意味着不假。true那么，如果当前的分配没有证伪问题，为什么我们可以返回呢？

我实现我的 SAT 求解器的方式是，每当遇到使所有子句都为真的赋值时，我返回那个赋值，算法就完成了。但是由于对于给定的赋值，所有子句都必须为真才能成为问题的解决方案，我不明白，true如果赋值刚好满足问题，怎么能返回（我假设我弄错了在这里，但是既然如果Φ是一致的，那么就意味着它不是假的，但它仍然可以是不可判定的？）。

DPLL SAT 求解器通常应用Phase Saving启发式算法。这个想法是记住每个变量的最后一次赋值并在分支中 首先使用它。

为了试验分支极性和相位节省的效果，我尝试了几个 SAT 求解器并修改了相位设置。都是Windows 64 位端口，以单线程模式运行。我总是使用中等复杂度的相同示例输入（5619 个变量，11261 个子句，在解决方案中，所有变量的 4% 为真，96% 为假）。

下面列出了生成的运行时间：

这可能只是（坏）运气，但差异非常大。在我的例子中， MiniSat的表现优于所有现代求解器，这让我感到特别惊讶。

我的问题：

对这些差异有任何解释吗？
极性和相位节省的最佳实践？