<p>The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General resolution is exponentially more powerful than tree-like resolution, as shown for example by <a href="http://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/BIW03/biw03.ps">Ben-Sasson, Impagliazzo and Wigderson</a>. The concept has also been considered for other proof systems – just search for "tree-like X", where X is a proof system interesting you. In the particular case of resolution, there are other restrictions that can be considered. See for example a paper of <a href="http://theoryofcomputing.org/articles/v003a005/v003a005.pdf">Alekhnovich, Johannsen, Pitassi and Urquhart</a> regarding regular resolution.</p>

<p>Tree-like resolution is especially important since traditional implementations of DPLL correspond to tree-like resolution refutations. The technique of clause learning, which is important in practice, corresponds to allowing general DAGs. Hence the structure of the proof DAG is also strongly dependent on the algorithm generating it.</p>

CC BY-SA 3.0
2015-01-20T06:50:00.800Z
It's also worth noting that tree-like Frege is equivalent to Frege.
Joshua Grochow
CC BY-SA 3.0
2015-01-18T21:08:22.897Z
2015-01-18T21:08:22.897Z
Yuval Filmus
<p><a href="http://dx.doi.org/10.1007/978-3-642-40313-2_62">Müller and Szeider</a> study Resolution proofs where the proof DAG has bounded tree-width or bounded path-width (for suitable extensions of these graph complexity measures to directed graphs.) </p>

<p>They show that the path-width of the DAG is essentially the same as the space complexity of the proof, and define a generalized notion of proof space which is equivalent to the tree-width.  </p>

CC BY-SA 3.0
2015-12-18T10:05:02.580Z
2015-12-18T10:05:02.580Z
Jan Johannsen
<p>For strong enough proof systems the graph representation of a proof in the system seems less consequential, since (as Joshua Grochow already commented), DAG-like and tree-like Frege proofs are polynomially equivalent (see Krajicek's 1995 <a href="http://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/bounded-arithmetic-propositional-logic-and-complexity-theory">monograph</a> for a proof of this fact). </p>

<p>For weaker proof systems such as resolution, tree-like is exponentially weaker than DAG-like proofs (as Yuval Filmus described above).</p>

<p>Beckmann and Buss <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/proofheight/index.html">[1]</a> (following Beckmann <a href="http://eccc.hpi-web.de/eccc-reports/2003/TR03-034/">[2]</a>) considered restricting the <strong>height</strong> (equivalently, depth) of the proof-graph of constant-depth Frege proofs and investigated the relationship between DAG-like, tree-size and height of constant depth Frege proofs. (Note the distinction between restricting the depth of the proof-graph and restricting the depth of a circuit appearing in a proof-line). </p>

<p>There might also be separations between tree-like and DAG-like Nullstellensatz (and polynomial calculus) proofs, which I currently don't remember.</p>

CC BY-SA 4.0
2024-07-17T20:05:05.453Z
Are DAG-like and tree-like Extended Resolution proofs polynomially equivalent for the same reason?
botsina
CC BY-SA 3.0
2015-12-21T21:22:05.727Z
2015-12-21T22:54:27.887Z
2015-12-21T22:54:27.887Z
Iddo Tzameret
<p>Proof complexity is a most basic area of computational complexity theory. An ultimate purpose of this area is to prove <span class="math-container">$NP\neq coNP$</span>, that is, any prover cannot give a proof of unsatisfiability of given input formula.</p>
<p>A graph is one of formal model of proofs.  My question is about further restriction to this model.</p>
<p>A proof is represented as a DAG. Nodes with fan-in 0 have axiom-labels. The unique node with fan-out 0 corresponds to &quot;false.&quot; For given input rules of deduction, each node which has both in-degree and out-degree has the  label representing proposition.</p>
<p>My question is:</p>
<blockquote>
<p>Are there proof systems and related researches in the case that the class of proof-DAGs are restricted?
Papers, survey, and lecture note are welcome.</p>
<p>Do Proof Systems which are previously studied such as Nullstellensatz, Resolution, LS, AC0 Frege, RES(k), Polynomial Caluculus, and Cutting Planes, have some graph theoretic characterization??</p>
</blockquote>

<cc.complexity-theory><reference-request><graph-theory><np><proof-complexity>
Graph theoretic restriction to Proofs in Proof Complexity Theory
shen
# Graph theoretic restriction to Proofs in Proof Complexity Theory

(Asked by: username_0 on 2015-01-18)

Proof complexity is a most basic area of computational complexity theory. An ultimate purpose of this area is to prove $NP\neq coNP$, that is, any prover cannot give a proof of unsatisfiability of given input formula.

A graph is one of formal model of proofs. My question is about further restriction to this model.

A proof is represented as a DAG. Nodes with fan-in 0 have axiom-labels. The unique node with fan-out 0 corresponds to "false." For given input rules of deduction, each node which has both in-degree and out-degree has the label representing proposition.

My question is:

> Are there proof systems and related researches in the case that the class of proof-DAGs are restricted?
> Papers, survey, and lecture note are welcome.
>
> Do Proof Systems which are previously studied such as Nullstellensatz, Resolution, LS, AC0 Frege, RES(k), Polynomial Caluculus, and Cutting Planes, have some graph theoretic characterization??

**Tags:** cc.complexity-theory, reference-request, graph-theory, np, proof-complexity

---

## 3 answers

### Answer by username_1 on 2015-01-18. Score: 19

The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General resolution is exponentially more powerful than tree-like resolution, as shown for example by [Ben-Sasson, Impagliazzo and Wigderson](http://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/BIW03/biw03.ps). The concept has also been considered for other proof systems – just search for "tree-like X", where X is a proof system interesting you. In the particular case of resolution, there are other restrictions that can be considered. See for example a paper of [Alekhnovich, Johannsen, Pitassi and Urquhart](http://theoryofcomputing.org/articles/v003a005/v003a005.pdf) regarding regular resolution.

Tree-like resolution is especially important since traditional implementations of DPLL correspond to tree-like resolution refutations. The technique of clause learning, which is important in practice, corresponds to allowing general DAGs. Hence the structure of the proof DAG is also strongly dependent on the algorithm generating it.

> **Comments:**
> **username_2**: It's also worth noting that tree-like Frege is equivalent to Frege.  

---

### Answer by username_3 on 2015-12-18. Score: 8

[Müller and Szeider](http://dx.doi.org/10.1007/978-3-642-40313-2_62) study Resolution proofs where the proof DAG has bounded tree-width or bounded path-width (for suitable extensions of these graph complexity measures to directed graphs.)

They show that the path-width of the DAG is essentially the same as the space complexity of the proof, and define a generalized notion of proof space which is equivalent to the tree-width.


---

### Answer by username_4 on 2015-12-21. Score: 7

For strong enough proof systems the graph representation of a proof in the system seems less consequential, since (as Joshua Grochow already commented), DAG-like and tree-like Frege proofs are polynomially equivalent (see Krajicek's 1995 [monograph](http://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/bounded-arithmetic-propositional-logic-and-complexity-theory) for a proof of this fact).

For weaker proof systems such as resolution, tree-like is exponentially weaker than DAG-like proofs (as Yuval Filmus described above).

Beckmann and Buss [[1]](http://www.math.ucsd.edu/~sbuss/ResearchWeb/proofheight/index.html) (following Beckmann [[2]](http://eccc.hpi-web.de/eccc-reports/2003/TR03-034/)) considered restricting the **height** (equivalently, depth) of the proof-graph of constant-depth Frege proofs and investigated the relationship between DAG-like, tree-size and height of constant depth Frege proofs. (Note the distinction between restricting the depth of the proof-graph and restricting the depth of a circuit appearing in a proof-line).

There might also be separations between tree-like and DAG-like Nullstellensatz (and polynomial calculus) proofs, which I currently don't remember.

> **Comments:**
> **username_5**: Are DAG-like and tree-like Extended Resolution proofs polynomially equivalent for the same reason?  

---

