comparative efficiency of method for automated reasoning
based on measuring the size of the proofs
method A p-simulates B if every proof in B can be translated to a similar-size proof in A
where:
every DPLL proof can be turned into a resolution proof
disregard unit propagation for now
part of a recursive tree
(X's omitted, numbers added to nodes to clarify exposition)
start from node 1
some clause c is false in node 1
assignments in 1 and 3 only differ on x3
c is false in 1,
if does not contain x3
⇒ it is false in 3
⇒ it contains x3...
... negated, because c is false in 1
the clause that is false in 1 contains ¬x3
same reason: clause falsified in 2 contains x3
the two clauses in 1 and 2 contain ¬x3 and x3, resp.
they resolve
write result in 3
clause falsified in 4 contains ¬x5
does A∨B necessarily contain x5?
5 and 3 only differ for x5=false
if A∨B does not contain x5, neither ¬x3∨A nor x3∨B do
attach 3 to 6:
otherwise, A∨B contains x5
it is something like x5∨D
resolve again
point is:
in the leaves: clauses false ⇒ made of assigned variables
each resolution removes a variable that is assigned
⇒ in the root: empty clause ⊥
proved that:
for each backtracking tree there exists a resolution tree of the same size or smaller
above, only falsified clauses matter
therefore: same result holds for DPLL
for each backtracking proof (or DPLL proof) there exists a similar-size one for resolution
resolution p-simulates both DPLL and backtracking
converse?
there are formulae that:
(short/large=relative size is exponential)
Hilbert system p-simulates resolution
not the other way around
therefore: Hilbert also p-simulates DPLL but not the converse