Resolution proof reduction via local context rewriting: Difference between revisions

Revision as of 05:56, 3 April 2012

Latest revision as of 14:48, 16 January 2024

(11 intermediate revisions by 10 users not shown)

Line 1:

AIn technique[[proof fortheory]], an area of [[mathematical logic]], '''resolution proof reduction via local context rewriting''' wasis proposeda bytechnique Simonefor Rollini,resolution Roberto[[proof Bruttomessocompression|proof andreduction]] Natashavia Sharyginalocal in their paper "An Efficient and Flexible Approachcontext to Resolution Proof Reduction"[[rewriting]].<ref name=Simone>Simone, S.F. ; Brutomesso, R. ; Sharygina, N. "An Efficient and Flexible Approach to Resolution Proof Reduction". 6th Haifa Verification Conference, 2010.</ref>. This [[proof compression]] method was presented as an algorithm named ''ReduceAndReconstruct'', that operates as a post-processprocessing onof [[resolution (logic)|resolution]] proofs.

ReduceAndReconstruct is based on a set of local proof rewriting rules that transform a subproof into aan equivalent or stronger one .<ref name=Simone />. Each rule is defined to match a specific context.

A context (as defined by Simone et al <ref name=Simone />) involves two pivots (<math>p</math> and <math>q</math>) and five clauses (<math>\alpha</math>, <math>\beta</math>, <math>\gamma</math>, <math>\delta</math> and <math>\eta</math>). The structure of a context is shown in ({{EquationNote|1}}). Note that this implyimplies that <math>p</math> is contained in <math>\beta</math> and <math>\gamma</math> (with opposite polarity) and <math>q</math> is contained in <math>\delta</math> and <math>\alpha</math> (also with opposite polarity).

{{NumBlk|:|<math>\cfrac{\cfrac{\beta \qquad \gamma}{\delta} \, p \qquad \alpha}{\eta} \, q</math>|{{EquationRef|1}}}}

The table below shows the rewriting rules proposed by Simone ''et al .''.<ref name=Simone />. The idea of the algorithm is to reduce proof size by opportunistically applying these rules.

{| class="wikitable"

Line 14:

|-

| Case A1: <math>s \notin \alpha, t \in \gamma</math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s} tD}{tCD} \, \operatorname{var}(s) \qquad \overline{t} E}{CDE} \, \operatorname{var}(t) \Rightarrow

\cfrac{\cfrac{stC \qquad \overline{t} E}{sCE}\, \operatorname{var}(t) \qquad \cfrac{\overline{t} E \qquad \overline{s} tD}{\overline{s}DE}\, \operatorname{var}(t)}{CDE} \, \operatorname{var}(s)</math>

|-

| Case A2: <math>s \notin \alpha, t \notin \gamma</math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s} D}{tCD} \, \operatorname{var}(s) \qquad \overline{t} E}{CDE} \, \operatorname{var}(t) \Rightarrow

\cfrac{\cfrac{stC \qquad \overline{t} E}{sCE} \, \operatorname{var}(t) \qquad \overline{s} D}{CDE} \, \operatorname{var}(s)</math>

|-

| Case B1: <math>s \in \alpha, t \in \gamma</math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s}tD}{tCD} \, \operatorname{var}(s) \qquad s \overline{t} E}{sCDE} \, \operatorname{var}(t) \Rightarrow

\cfrac{stC \qquad s \overline{t} E}{sCE}\, \operatorname{var}(t)</math>

|-

| Case B2: <math>s \in \alpha, t \notin \gamma</math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s}D}{tDC} \, \operatorname{var}(s) \qquad s \overline{t} E}{sCDE} \, \operatorname{var}(t) \Rightarrow

\cfrac{\cfrac{stC \qquad s \overline{t} E}{sCE} \, \operatorname{var}(t) \qquad \overline{s} D}{CDE} \, \operatorname{var}(s)</math>

|-

| Case B3: <math>\overline{s} \in \alpha, t \notin \gamma</math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s}D}{tDC} \, \operatorname{var}(s) \qquad \overline{s} \overline{t} E}{\overline{s} CDE} \, \operatorname{var}(t) \Rightarrow

\overline{s} D</math>

|-

| Case A1' ||

<math>\cfrac{\cfrac{stC \qquad \overline{s} tD}{tCD} \, \operatorname{var}(s) \qquad \overline{t} E}{CDE} \, \operatorname{var}(t) \Leftarrow

\cfrac{\cfrac{stC \qquad \overline{t} E}{sCE}\, \operatorname{var}(t) \qquad \cfrac{\overline{t} E \qquad \overline{s} tD}{\overline{s}DE}\, \operatorname{var}(t)}{CDE} \, \operatorname{var}(s)</math>

|-

| Case B2': <math>t \notin \gamma </math> ||

<math>\cfrac{\cfrac{stC \qquad \overline{s} D}{tCD} \, \operatorname{var}(s) \qquad s \overline{t} E}{sCDE} \, \operatorname{var}(t) \Rightarrow

\cfrac{stC \qquad s \overline{t} E}{sCE}\, \operatorname{var}(t)</math>

|}

Note that theThe first five rules were introduced in aan earlier paper .<ref name=Bruttomesso>Bruttomesso, R. ; Rollini, S. ; Sharygina, N.; Tsitovich, A. "Flexible Interpolation with Local Proof Transformations". The International Conference on Computer-Aided Design, 2010.</ref>. In addition, the following is worth mentioning:

* Rule A2 does not perform any reduction on its own. However, it is still useful, because of its "shuffling" effect that can create new opportunities for applying the other rules;

* Rule A1 is not used in practice, because it may increase proof size;

* Rules B1, B2, B2' and B3 are directly resposibleresponsible for the reduction, as they produce a transformed root clause stronger than the original one;

* The application of a B rule may lead to aan illegal proof (see the example below), as some literals missing in the transformed root clause may be involved in another resolution step along the path to the proof root. Therefore, the algorithm also has to "reconstruct" a legal proof when this happen.

The following example (extracted from <ref name=Simone />) shows a situation where the proof becomes illegal after the application of B2' rule:

{{NumBlk|:|

Line 63:

</math>|{{EquationRef|3}}}}

Note that theThe proof is now illegal because the literal <math>o</math> is missing from the transformed root clause. To reconstruct the proof, one can remove <math>o</math> together with the last resolution step (that is now redudantredundant). The final result is the following legal (and stronger) proof:

{{NumBlk|:|

Line 70:

</math>|{{EquationRef|4}}}}

Simone et al <ref name=Simone /> shows aA further reduction of this proof by applying rule A2 to create a new opportunity to apply rule B2'.<ref name=Simone />

NoteThere thatare thereusually is usuallya huge number of contexts where rule A2 may be applied, so an exaustiveexhaustive approach is not feasible in general. Therefore, Simone et alOne proposal<ref name=Simone /> proposeis to execute <code>ReduceAndReconstruct </code> as a loop with two termination criteria: number of iterations and a timeout (what is reached first). The pseudocode (adapted from <ref name=Simone />) below shows this.

1 '''function''' ReduceAndReconstruct(''<math>\pi</math>'' ''/* a proof */'', ''timelimit'', ''maxIterations''):

Line 82:

7 '''end function'''

<code>ReduceAndReconstruct</code> uses the function <code>ReduceAndReconstructLoop</code>, which is specified below. Note that theThe first part of the algorithm does a [[topological ordering]] of the [[resolution graph]] (considering that edges goes from antecedentes to resolvents). This is done to ensure that each node is visited after its antecedents (this way, broken resolution steps are always found and fixed) .<ref name=Simone />.

1 '''function''' ReduceAndReconstructLoop(''<math>\pi</math>'' ''/* a proof */''):

Line 88:

3 '''for each''' node <math>n</math> '''in''' ''TS''

4 '''if''' <math>n</math> is not a leaf

5 '''if''' ''<math>n_\text{piv} \in n_\text{clause}^\text{left}</math> and <math>\overline{n_\text{piv}} \in n_\text{clause}^\text{right}</math>'' '''then'''

6 <math>n_\text{clause}</math> = Resolution(<math>n_\text{clause}^\text{left}</math>, <math>n_\text{clause}^\text{right}</math>);

7 Determine left context of <math>n</math>, if any;

8 Determine right context of <math>n</math>, if any;

9 Heuristically choose one context (if any) and apply the corresponding rule;

10 '''else if''' ''<math>n_\text{piv} \notin n_\text{clause}^\text{left}</math> and <math>\overline{n_\text{piv}} \in n_\text{clause}^\text{right}</math>'' '''then'''

11 Substitute <math>n</math> with <math>n^\text{left}</math>;

12 '''else if''' ''<math>n_\text{piv} \in n_\text{clause}^\text{left}</math> and <math>\overline{n_\text{piv}} \notin n_\text{clause}^\text{right}</math>'' '''then'''

13 Substitute <math>n</math> with <math>n^\text{right}</math>;

14 '''else if''' ''<math>n_\text{piv} \notin n_\text{clause}^\text{left}</math> and <math>\overline{n_\text{piv}} \notin n_\text{clause}^\text{right}</math>'' '''then'''

15 Heuristically choose an antecedent <math>n^\text{left}</math> or <math>n^\text{right}</math>;

16 Substitute <math>n</math> with <math>n^\text{left}</math> or <math>n^\text{right}</math>;

17 '''end for'''

18 '''end function'''

Another point that worth mentioning is that ifIf the input proof is not a tree (in general, resolution graphs are [[directed acyclic graph|directed acyclic graphs]]s), then the clause <math>\delta</math> of a context may be involved in more than one resolution step. In this case, to ensure that aan application of a rewriting rule is not going to interfere with other resolution steps, a safe solution is to create a copy of the node represented by clause <math>\delta</math> .<ref name=Simone />. Note that thisThis solution increases proof size and some caution is needed when doing this.

Moreover, theThe [[heuristic]] for rule selection is important to achieve a good compression performance. Simone ''et al.'' <ref name=Simone /> use the following order of preference for the rules (if applicable to the given context): B2 > B3 > { B2', B1 } > A1' > A2 (X > Y means that X is preferred over Y).

Experiments have shown that ReduceAndReconstruct alone has a worse compression/time ratio than the algorithm [[RecyclePivots]] .<ref name=Bar-Ilan>Bar-Ilan, O. ; Fuhrmann, O. ; Hoory, S. ; Shacham, O. ; Strichman, O. "Linear-Time Reductions of Resolution Proofs". HVC, 2008.</ref>. However, while RecyclePivots can be applied only once to a proof, ReduceAndReconstruct may be applied multiple times to produce a better compression. An attempt to combine ReduceAndReconstruct and RecyclePivots algorithms has leadled to good results .<ref name=Simone />.

==Notes==

{{reflist}}

[[Category:Articles with example pseudocode]]

[[Category:Proof theory]]