DPLL算法定义 [英] DPLL algorithm definition

问题描述

我有一些问题了解DPLL算法，我想知道是否有人能解释给我，因为我觉得我的理解是不正确。

I am having some problems understanding the DPLL algorithm and I was wondering if anyone could explain it to me because I think my understanding is incorrect.

我的理解是这样的，我需要一些集文字的，如果有的每一个条款是真实的模型是真实的，但如果某些条款是假，那么该模型是假的。

The way I understand it is, I take some set of literals and if some every clause is true the model is true but if some clause is false then the model is false.

我递归查询的模型，寻找一个单元子句中，如果有一个我设置的值，该单元条款，使之真，则更新模型。删除了，现在真正的所有条款，并删除它们现在假的。

I recursively check the model by looking for a unit clause, if there is one I set the value for that unit clause to make it true, then update the model. Removing all clauses that are now true and remove all literals which are now false.

在，已经没有单位的条款，我选择的任何其他文字，并为文字，这使得它真实，使之假，然后再删除其现在真实，所有的条款而现在假的所有文字赋值。

When there are no unit clauses left, I chose any other literal and assign values for that literal which make it true and make it false, then again remove all clauses which are now true and all literals which are now false.

推荐答案

DPLL需要一个问题，析取范式来加以说明，即作为一套条款，每个都必须得到满足。

DPLL requires a problem to be stated in disjunctive normal form, that is, as a set of clauses, each of which must be satisfied.

每个子句是一个集文字的 {L1，L2，...，LN} ，再presenting这些文字的脱节（即至少1文字必须是真实的条款得到满足）。

Each clause is a set of literals {l1, l2, ..., ln}, representing the disjunction of those literals (i.e., at least one literal must be true for the clause to be satisfied).

每个文字→称，一些变量是真实的（ X ），或者说，它是假的（〜X ）。

Each literal l asserts that some variable is true (x) or that it is false (~x).

如果任何文字是在第true，则该条款满足了。

If any literal is true in a clause, then the clause is satisfied.

如果在子句中所有的文字都是假的，那么该条款是不可满足的，所以这个问题是不可满足的。

If all literals in a clause are false, then the clause is unsatisfiable and hence the problem is unsatisfiable.

一个解决方案是真/假值赋值给变量，使得每个条款都感到满意。 DPLL的算法是这样的解决方案的一个优化的搜索

A solution is an assignment of true/false values to the variables such that every clause is satisfied. The DPLL algorithm is an optimised search for such a solution.

DPLL基本上是三个战术之间交替的深度优先搜索。在，在搜索任何阶段有部分转让（即，值的变量的一些子集的分配）和一组未定条款（即，那些还没有被满足条款）。

DPLL is essentially a depth first search that alternates between three tactics. At any stage in the search there is a partial assignment (i.e., an assignment of values to some subset of the variables) and a set of undecided clauses (i.e., those clauses that have not yet been satisfied).

（1）第一个策略是纯文字消除：如果未分配变量 X 只出现在其正面的形式在一套未定条款（即文字〜X 并没有出现在任何地方），那么我们可以再补充 X =真我们的任务，并满足所有包含该条款文字 X （同​​样，如果 X 只出现在它的否定形式，〜X ，我们可以再补充 X =假我们的任务）。

(1) The first tactic is Pure Literal Elimination: if an unassigned variable x only appears in its positive form in the set of undecided clauses (i.e., the literal ~x doesn't appear anywhere) then we can just add x = true to our assignment and satisfy all the clauses containing the literal x (similarly if x only appears in its negative form, ~x, we can just add x = false to our assignment).

（2）第二个策略是单位传播：如果所有，但在犹豫不决条款的文字之一，是假的，那么剩下的一个必须是真实的。如果剩余的文字是 X ，我们添加 X =真我们的任务;如果剩余的文字是〜X ，我们添加 X =假我们的任务。这种分配可能会导致更多的机会进行单元传播。

(2) The second tactic is Unit Propagation: if all but one of the literals in an undecided clause are false, then the remaining one must be true. If the remaining literal is x, we add x = true to our assignment; if the remaining literal is ~x, we add x = false to our assignment. This assignment can lead to further opportunities for unit propagation.

（3）第三个策略是简单地选择一个未分配的变量 X 和分支搜索：一面努力 X =真，其他试图 X =假。

(3) The third tactic is to simply choose an unassigned variable x and branch the search: one side trying x = true, the other trying x = false.

如果在我们结束了一个不可满足的子句那么任何时候，我们已经走进了死胡同，不得不原路返回。

If at any point we end up with an unsatisfiable clause then we have reached a dead end and have to backtrack.

有各种聪明进一步的优化，但是这是几乎所有的SAT求解器的核心。

There are all sorts of clever further optimisations, but this is the core of almost all SAT solvers.

希望这有助于。

这篇关于DPLL算法定义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！