Neu*_*ise 5 algorithm artificial-intelligence
我在理解DPLL算法时遇到了一些问题,我想知道是否有人可以向我解释,因为我认为我的理解是不正确的.
我理解它的方式是,我采用一些文字,如果某些每个子句都为真,则模型为真,但如果某个子句为假,则模型为假.
我通过查找一个单元子句递归检查模型,如果有一个我设置了该单元子句的值使其成为真,则更新模型.删除现在为true的所有子句并删除现在为false的所有文字.
如果没有单位子句,我选择任何其他文字并为该文字指定值使其成立并使其成为假,然后再次删除现在为真的所有子句以及现在为假的所有文字.
DPLL要求以分离正常形式陈述问题,即作为一组条款,每个条款必须满足.
每个子句都是一组文字{l1, l2, ..., ln},表示这些文字的分离(即,对于要满足的子句,至少有一个文字必须为真).
每个文字都l断言某些变量是true(x)或者是false(~x).
如果子句中的任何文字都为真,那么该子句就满足了.
如果一个子句中的所有文字都是假的,那么该条款是不可满足的,因此问题是不可满足的.
解决方案是将变量的真/假值赋值给每个子句.DPLL算法是对这种解决方案的优化搜索.
DPLL本质上是深度优先搜索,在三种策略之间交替.在搜索的任何阶段,都存在部分赋值(即,对某些变量子集赋值)和一组未决条款(即那些尚未满足的子句).
(1)第一个策略是Pure Literal Elimination:如果一个未分配的变量x只在未确定的子句中以正面形式出现(即,文字~x不会出现在任何地方),那么我们可以添加x = true到我们的任务中并满足所有包含文字的子句x(类似地,如果x仅以其否定形式出现~x,我们可以添加x = false到我们的作业中).
(2)第二种策略是单位传播:如果一个未定的条款中的一个文字都是假的,那么剩下的一个必须是真的.如果剩下的文字是x,我们加入x = true我们的任务; 如果剩下的文字是~x,我们将添加x = false到我们的作业中.这一任务可以为单位传播带来更多机会.
(3)第三种策略是简单地选择一个未分配的变量x并对搜索进行分支:一方尝试x = true,另一方尝试x = false.
如果在任何时候我们最终得到一个不满意的条款,那么我们已经走到了死胡同并且不得不回溯.
有各种巧妙的进一步优化,但这是几乎所有SAT求解器的核心.
希望这可以帮助.