Return Search Algorithm

The first algorithm considered here is often called the Davis-Putnam algorithm in honor of the authors of the original article in which it was published, by Martin Davis and Hilary Putnam. Then this algorithm actually became one of the versions described by Davis, Logman and Loveland, so we will call it DPLL after the first letters of the names of all four authors. At the input, the DPLL algorithm takes a statement in conjunctive normal form — a statement represented as a set of expressions. Like Backtracking-Search and TT-Entails?, It actually performs a recursive brute-force search of all possible models. But in this algorithm, the three improvements described below are implemented, and by this it differs from the simple scheme used in the TT-Entails? Algorithm.

Early completion . The algorithm detects whether a given statement should be true or false, even with a partially completed model. An expression is true if any of its literals is true, even though truth values ​​are not yet defined for other literals; therefore, the truth of the whole statement as a whole can be judged even before the model has been fully compiled. For example, the statement (A v B) l (A v C) is true if the literal A is true, regardless of the values ​​of the literals B and C. Similarly, the statement is false if any of its expressions are false, and this happens if each literal This expression is false. Again, such a situation may occur long before the model is fully compiled. Early completion eliminates the need to explore entire subtrees in the search space.

Heuristics is a pure symbol . A pure symbol is a symbol that always appears with the same “sign” in all expressions. For example, in the three expressions (A v ¬B), (¬B v ¬C) and (C v A), the symbol A is pure, because it appears only as positive literals, you can also consider the pure symbol, which appears only in as negative literals, and the character C is considered unclean. It can easily be shown that if a statement has a model, then it is a model with pure characters, the values ​​of which are assigned so that their literals take the value true, since under this condition no expression can become false. It should be noted that when determining the purity of a symbol, the algorithm can ignore expressions in relation to which it is already known that they are true in the model that has been compiled up to now. For example, if the model contains the assignment B - false, then the expression (¬B v ¬С) is already true, and the symbol C becomes pure, because it is present only in the expression (C v A).

Heuristics of a single expression . A single expression was previously defined as an expression with only one literal. In the context of the DPLL algorithm, it also refers to expressions in which all but one of the literals in this model have already been set to false. For example, if the model contains the assignment B = false, then the expression (В v ¬C) becomes a single expression, because it is equivalent to the expression (False v ¬C), or simply ¬C. Obviously, in order for this expression to accept the true value, the literal C must be assigned the value false. The heuristic of a single expression provides for the assignment of values ​​to all such characters before the transition to processing the rest of the statement. One of the important consequences of this heuristic is that any attempt to prove (by refutation) the truth of a literal that is already in the knowledge base immediately leads to success. It should also be noted that assigning a value to one single expression can lead to the creation of another single expression; for example, after assigning C to the value false, the single expression becomes (C v A), which entails assigning the true value to the symbol A. Such a "cascading" distribution of forced assignments is called "&. the distribution of single expressions. Horn expressions, but in reality, if the statement in question in conjunctive normal form contains only Horn expressions, then the DPLL algorithm essentially reduces to a direct logical algorithm one output.

The DPLL algorithm is shown in the listing. This listing shows the most important structural part of the algorithm, which describes the search process itself, but does not provide the data structures that must be followed to ensure the effectiveness of each search step, and also excludes all programmer tricks that could be introduced to improve performance: exploring expressions, variable selection heuristics and randomized restart operations. After incorporating all these enhancements, the DPLL algorithm, despite its venerable age, becomes one of the fastest feasibility verification algorithms ever developed. In particular, the Chaff implementation of this algorithm is used to solve problems of checking the quality of hardware with a million variables.

DPLL algorithm to test the feasibility of a statement in propositional logic. The principles of the functions of the Find-Pure-Symbol and Find-Unit-Clause are described in the text; each of them returns a symbol (or null value), as well as a truth value, which must be assigned to this symbol. Like tt-entails ?, this algorithm works with partially compiled models.

function DPLL-Satisfiable? (s) returns true or false

   inputs : s, statement in propositional logic

clauses <- set of expressions of the statement s, transformed

to CNF submission form

symbols <- list of propositional symbols in the statement s

return DPLL {clausesf symbols, [])

function DPLL (clauses, symbols, model) returns true or false

   if every clauses clause is true

in model

then return true

   if some clauses expression is false

in model

then return false

P, value <- Find-Pure-Symbol (symbols, clauses, model)

   if the value of P is not empty

then return DPLL (clauses, symbols-P, Extend (P, value, model))

P, value <- Find-Unit-Clause (clauses, model)

   if the value of P is not empty

then return DPLL (clauses, symbols-P, Extend (P, value, model))

P <r- First (symbols); rest <- Rest (symbols)

return DPLL (clauses, rest, Extend (P, true, model)) or

DPLL (clauses, rest, Extend (P, false, model))