10
$\begingroup$

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??

Improve this question
$\endgroup$

3 Answers 3

Reset to default
19
$\begingroup$

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. 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 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.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ It's also worth noting that tree-like Frege is equivalent to Frege. $\endgroup$
    – Joshua Grochow
    Jan 20, 2015 at 6:50
8
$\begingroup$

Müller and Szeider 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.

Improve this answer
$\endgroup$
6
$\begingroup$

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 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] (following Beckmann [2]) 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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.