Long-distance resolution for quantified boolean formula (QBF) solving was introduced in 2002 by Zhang and Malik, but has been controversial for the following decade, because it derives and uses tautologous clauses. Balabanov and Jiang (2012) gave a set of proof rules (called LDQ-resolution) that include long-distance resolution with conditions, but did not attach any “meaning” (i.e., semantic interpretation) to the derived tautologous clauses. Egly, Lonsing and Widl (2013) showed that the QBF certificate extraction algorithm of Goutltiaeva, Van Gelder and Bacchus (2011) could be applied with correct results to LDQ refutations. These results and others have brought LDQ-resolution back into the mainstream. This paper introduces partial boolean functions (pbfs) and develops a semantic interpretation for universal literals in QBF clauses. It develops LDP-resolution, which is refutationally complete for QBF formulas in prenex conjunction normal form (PCNF). LDP-resolution is shown to derive only logical consequences.
原文链接
分享
引用
