DPLL 算法伪代码

以下是DPLL算法的伪代码：

function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause l in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));
end function

其中，Φ表示一个CNF公式，unit-propagate(l, Φ)表示将l赋值为真，并根据这个赋值更新Φ中的所有子句，pure-literal-assign(l, Φ)表示将所有包含l的子句都赋值为真，choose-literal(Φ)表示从Φ中选择一个未被赋值的文字。