问题标签 [dpll]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

24 问题
Newest
Active
Bountied
318
Unanswered
0 投票
2 回答
412 浏览

backtracking - How to implement non chronological backtracking

I'm working on a CDCL SAT-Solver. I don't know how to implement non-chronological backtracking. Is this even possible with recursion or is it only possible in a iterative approach.

Actually what i have done jet is implemented a DPLL Solver which works with recursion. The great differnece from DPLL and CDCL ist that the backracking in the tree is not chronological. Is it even possible to implement something like this with recursion. In my opionion i have two choices in the node of the binary-decision-tree if one of to path leads i a conlict:

  1. I try the other path -> but then it would be the same like the DPLL, means a chronological backtracking
  2. I return: But then i will never come back to this node.

So am i missing here something. Could it be that the only option is to implement it iterativly?

0 投票
1 回答
330 浏览

prolog - 如何从prolog中的变量列表中删除变量？

我想实现 DPLL 算法。因此，我必须删除其他变量列表中所有出现的变量，例如删除neg(X)应该[neg(X), pos(X), neg(Y), pos(Y)]返回[pos(X), neg(Y), pos(Y)]。我尝试了一些内置谓词，例如 exclude/3 或 delete/3 但都给我留下了假设X = Y和结果[pos(X), pos(Y)]，删除了所有 neg(_)，但我只希望删除 neg(X) 而不是 neg(Y) . 这有可能吗？

0 投票
0 回答
10 浏览

artificial-intelligence - 这些算法中的哪一种是基于 DFS 的？（深度优先搜索）？

我很难找出这些算法中的哪一个是基于 DFS 的？

  1. GSAT
  2. 锁相环
  3. 爬山
  4. 冲突-最小

我对 CONFLICTS-MIN 和 DPLL 感到困惑。希望得到任何帮助！谢谢！

0 投票
0 回答
6 浏览

dpll - DPLL 结果是必然的吗？

我在理解下一个练习时遇到了问题。我们如何理解是否需要建议？

应用DPLL算法通过以下建议证明 ~ p 是必然的：

( ~q | ~r ) & ( ~q | r ) & ( ~p | q ) & p

q = 真

( ~q | ~r ) & ( ~q | r ) & p

删除~q

~r & r & p

r = 真

〜r＆p

删除~r

p 最终结果。

有人可以解释一下是否包含p以及为什么？


12345678910