Lower bounds for algebraic proof systems
|
Аннотация
1 Introduction 4
1.1 Our results 5
1.2 Organization of the paper 6
1.3 Remark about Ext-PC definition 6
2 Preliminaries 6
3 Lower bound 8
3.1 Lower bound over integers 8
3.2 Lower bound over rationals 9
4 Connection between Res-Lin, Ext-PCQ and Ext-PCQ 14
4.1 Ext-PCQ simulation of Res-Lin 15
4.2 Ext-PCQ cannot simulate square root derivation rule 17
1 Introduction 4
1.1 Our results 5
1.2 Organization of the paper 6
1.3 Remark about Ext-PC definition 6
2 Preliminaries 6
3 Lower bound 8
3.1 Lower bound over integers 8
3.2 Lower bound over rationals 9
4 Connection between Res-Lin, Ext-PCQ and Ext-PCQ 14
4.1 Ext-PCQ simulation of Res-Lin 15
4.2 Ext-PCQ cannot simulate square root derivation rule 17
In essence, the study of propositional proof complexity started with the work of Cook and Reckhow [9], which states that if there is a propositional proof system in which any unsatisfiable formula F has a short proof of unsatisfiability, then NP = CoNP. The first superpolynomial bound on the proof size was proved in a pioneering work of Tseitin [30] for regular resolution. Since then, many proof systems have been studied, some of them are logic-style (working with disjunctions, conjunctions, and other Boolean operations) and some of them are algebraic (working with arbitrary polynomials).
In this work, we consider extensions of two systems, an algebraic one and a logic-style one.
Logic-style systems. As it was mentioned before, the first superpolynomial bound on the proof size was proved in a work of Tseitin for regular resolution, which is a popular logic proof system. Lately, Haken [13] proved an exponential lower bound on the size of (unrestricted) Resolution refutation of the pigeonhole principle (PHP), expressing that there is no (total) injective map from a set with cardinality m to a set with cardinality n if m > n.
Since then, a stronger logic proof systems such as Frege systems were considered. But while exponential lower bounds for low-depth proof systems (both algebraic and logical ones) are known for decades, the situation with the higher depth proof systems is much worse. The present knowledge is limited to superpolynomial lower bounds for Frege systems over de Morgan basis (that is, without xor’s or equivalences) of depth up to ©(log(n)/ loglog(n)) [14] (see also [23] where a superpolynomial lower bound for systems of depth up to ©(y/log(n)) is proved).
Resolution with counting. Another approach to strengthen resolution is to use weak extensions in order to do some sort of counting. Res-Lin (defined in [24]) is a system working with disjunctions of linear equations, and can be viewed as a generalization of Resolution (we consider this system in the present paper). However, no truly exponential lower bounds are known for the size of refutations of formulas in CNF in (dag-like) systems that work over disjunctions of equations or inequalities (see [18] as the first paper defining these systems and containing partial results). Part and Tzameret [20] proved an exponential lower bound for (dag-like) Res-Lin refutations over Q for the binary value principle BVPn. Although this is the first exponential lower bound for this system, the instance does not correspond to a translation of formula in CNF.
Itsykson and Sokolov [17] considered another extension of the resolution proof system that operates with disjunctions of linear equalities over F2 named Res(®) and proved an exponential lower bound on the size of tree-like Res(®)-proofs.
Algebraic proof systems. Algebraic proof systems such as Nullstellensatz were developed to use some algebraic techniques of Razborov and Smolensky [25, 28] in the proof complexity case. Lower bounds for algebraic systems started with an exponential lower bound for the Nullstellensatz [2] system. The main system considered in this paper is based on the Polynomial Calculus system [6], which is a dynamic version of Nullstellensatz. Many exponential lower bounds are known for the size of Polynomial Calculus proofs for tautologies like the Pigeonhole Principle [26, 16] and Tseitin tautologies [3]. While most results concern the representation of Boolean values by 0 and 1, there are also exponential lower bounds over the {-1, +1} basis [29].
However, simple algebraic proof systems such as Nullstellensatz and Polynomial Calculus cannot simulate strong logic systems like Frege systems and thus cannot provide lower bounds for these systems. In order to fix this issue, strong extensions were considered: Grigoriev and Hirsch [11] considered algebraic systems over formulas. Grochow and Pitassi [12] introduced the Ideal Proof System, IPS, which can be considered as the version of Nullstellensatz where all polynomials are written as algebraic circuits (see also [21, 22] for earlier versions of this system).
Many other extensions of Polynomial Calculus and Nullstellensatz have been considered also. Buss, Impagliazzo, Krajicek, Pudlak, Razborov and Sgall [4] showed that there is a tight connection between the lengths of constant-depth Frege proofs with MODp gates and the length of Nullstellensatz refutations using extension axioms. Impagliazzo, Mouli and Pitassi [15] showed that a depth-3 extension of Polynomial Calculus called SHS-PC p-simulates semantic CP* (an inequalities-based system, Cutting Planes [10, 5] with coefficients written in unary) over Q. Also, they showed that a stronger extension of Polynomial Calculus, called Depth-k-PC, p-simulates Cutting Planes and another inequalities-based system Sum-of-Squares; the simulations can be conducted over Fpm for an arbitrary prime number p if m is sufficiently large. However, the question about proving a superpolynomial lower bound even on the size of SHS-PC refutations over any field remains open since it is not clear how to extend lower bound techniques such as size-degree tradeoff to this system.
1.1 Our results
We extend Polynomial Calculus with two additional rules. One rule allows us to take a square root (it was introduced by Grigoriev and Hirsch [11] in the context of transforming refutation proofs of non-Boolean formulas into derivation proofs; our motivation to take square roots is to consider an algebraic system that is at least as strong as Res-Lin even for non-Boolean formulas, see below). Another rule is an algebraic version of Tseitin’s extension rule, which allows us to introduce new variables that are equivalent to arbitrary depth algebraic circuits. We will denote our generalization of Polynomial Calculus as Ext-PC< Note that Ext-PC^ p-simulates Extended Frege system (since Ext- PC^ p-simulates Extended Resolution and Extended Resolution p-simulates Extended Frege [19]), but it’s not obvious how to p-simulate IPS refutations in Ext-PC^ (since IPS refutations polynomials are written as algebraic circuits and Ext-PC^ refutations are written explicitly as a sum of monomials).
In this work we give a partial positive answer to the question raised in [15] asking for a technique for proving size lower bounds on Polynomial Calculus without proving any degree lower bounds. However, our lower bound works only for field Q and the question about proving lower bounds over finite fields remains open. Also, we give a partial answer to another question raised in [15] by proving an exponential lower bound for the system with an extension rule even stronger than that in SHS-PC, which is another extension of Polynomial Calculus presented in the aforementioned work.
We consider the following subset-sum instance, called Binary Value Principle (BVPn) [1, 20]:
1 + xi + 2x2 + ... 2ra-1x„ = 0,
and prove an exponential lower bound for the size of Ext-PCQ refutations of BVPn. Note that Binary Value Principle does not correspond to the translation of any CNF formula and thus the question about proving the size lower bound on the refutation of formulas in CNF without proving degree lower bounds remains open.
Theorem 1.1. Any Ext-PCQ refutation of BVPn requires size 2Q(ra).
The technique we use for proving this lower bound is similar to the technique for proving the conditional IPS lower bound in [1]. However, since Ext-PC proof system is weaker than Ideal Proof System, we get an unconditional lower bound. The main idea of the conditional lower bound in [1] is to prove the complexity lower bound on the free term in the end of the IPS-refutation of BVPn over Z and then show that IPSZ simulates IPSq. One difference is that instead of concentrating on the complexity of computing the free term of the proof, we concentrate on the prime numbers being mentioned in the proof (and thus appearing as factors of the free term).
Then we consider Res-Lin and show that Ext-PCQ simulates Res-Lin and thus get an alternative lower bound for Res-Lin.
Corollary 1.2. Any Res-LinQ refutation of BVPn requires size 2Q(ra).
Note that while Part and Tzameret [20] prove an exponential lower bound on the number of lines in the proof, we prove a bound on the proof size (essentially, on the bit size of scalars appearing in the proof).
1.2 Organization of the paper
In Section 2 we recall the definition of Polynomial Calculus (PC) and give the definitions of Polynomial Calculus with square root (PO^) and Extended Polynomial Calculus with square root (Ext-PC^).
In Section 3 we prove an exponential lower bound on the size of Ext-PCQ refutations of BVPn. We start with considering derivations with integer coefficients (Ext-PCQ) and show that the free term in the end of such refutation of BVPn is not just large but also is divisible by all primes less than 2n (see Theorem 3.1). Then, in Theorem 3.4, we convert proofs over Q into proofs over Z without changing the set of primes mentioned in the proof and thus get an Ext-PCQ lower bound.
In Section 4 we show that Ext-PCQ simulates Res-Lin and thus we get an alternative lower bound for the size of Res-Lin refutations of BVPn.
1.3 Remark about Ext-PC definition
In the original bachelor work, Ext-PC proof system was defined slightly different. The “old” definition allowed us to introduce new variables that encode polynomials depending on the original variables only, which is slightly weaker approach than the present one. However, it turned out that with some modifications, one can use the same technique to prove lower bound for the proof system, in which new variables encode arbitrary algebraic circuits. So, after some discussions with Edward Hirsch, we decided to change the definition of Ext-PC proof system to the present one.
In this work, we consider extensions of two systems, an algebraic one and a logic-style one.
Logic-style systems. As it was mentioned before, the first superpolynomial bound on the proof size was proved in a work of Tseitin for regular resolution, which is a popular logic proof system. Lately, Haken [13] proved an exponential lower bound on the size of (unrestricted) Resolution refutation of the pigeonhole principle (PHP), expressing that there is no (total) injective map from a set with cardinality m to a set with cardinality n if m > n.
Since then, a stronger logic proof systems such as Frege systems were considered. But while exponential lower bounds for low-depth proof systems (both algebraic and logical ones) are known for decades, the situation with the higher depth proof systems is much worse. The present knowledge is limited to superpolynomial lower bounds for Frege systems over de Morgan basis (that is, without xor’s or equivalences) of depth up to ©(log(n)/ loglog(n)) [14] (see also [23] where a superpolynomial lower bound for systems of depth up to ©(y/log(n)) is proved).
Resolution with counting. Another approach to strengthen resolution is to use weak extensions in order to do some sort of counting. Res-Lin (defined in [24]) is a system working with disjunctions of linear equations, and can be viewed as a generalization of Resolution (we consider this system in the present paper). However, no truly exponential lower bounds are known for the size of refutations of formulas in CNF in (dag-like) systems that work over disjunctions of equations or inequalities (see [18] as the first paper defining these systems and containing partial results). Part and Tzameret [20] proved an exponential lower bound for (dag-like) Res-Lin refutations over Q for the binary value principle BVPn. Although this is the first exponential lower bound for this system, the instance does not correspond to a translation of formula in CNF.
Itsykson and Sokolov [17] considered another extension of the resolution proof system that operates with disjunctions of linear equalities over F2 named Res(®) and proved an exponential lower bound on the size of tree-like Res(®)-proofs.
Algebraic proof systems. Algebraic proof systems such as Nullstellensatz were developed to use some algebraic techniques of Razborov and Smolensky [25, 28] in the proof complexity case. Lower bounds for algebraic systems started with an exponential lower bound for the Nullstellensatz [2] system. The main system considered in this paper is based on the Polynomial Calculus system [6], which is a dynamic version of Nullstellensatz. Many exponential lower bounds are known for the size of Polynomial Calculus proofs for tautologies like the Pigeonhole Principle [26, 16] and Tseitin tautologies [3]. While most results concern the representation of Boolean values by 0 and 1, there are also exponential lower bounds over the {-1, +1} basis [29].
However, simple algebraic proof systems such as Nullstellensatz and Polynomial Calculus cannot simulate strong logic systems like Frege systems and thus cannot provide lower bounds for these systems. In order to fix this issue, strong extensions were considered: Grigoriev and Hirsch [11] considered algebraic systems over formulas. Grochow and Pitassi [12] introduced the Ideal Proof System, IPS, which can be considered as the version of Nullstellensatz where all polynomials are written as algebraic circuits (see also [21, 22] for earlier versions of this system).
Many other extensions of Polynomial Calculus and Nullstellensatz have been considered also. Buss, Impagliazzo, Krajicek, Pudlak, Razborov and Sgall [4] showed that there is a tight connection between the lengths of constant-depth Frege proofs with MODp gates and the length of Nullstellensatz refutations using extension axioms. Impagliazzo, Mouli and Pitassi [15] showed that a depth-3 extension of Polynomial Calculus called SHS-PC p-simulates semantic CP* (an inequalities-based system, Cutting Planes [10, 5] with coefficients written in unary) over Q. Also, they showed that a stronger extension of Polynomial Calculus, called Depth-k-PC, p-simulates Cutting Planes and another inequalities-based system Sum-of-Squares; the simulations can be conducted over Fpm for an arbitrary prime number p if m is sufficiently large. However, the question about proving a superpolynomial lower bound even on the size of SHS-PC refutations over any field remains open since it is not clear how to extend lower bound techniques such as size-degree tradeoff to this system.
1.1 Our results
We extend Polynomial Calculus with two additional rules. One rule allows us to take a square root (it was introduced by Grigoriev and Hirsch [11] in the context of transforming refutation proofs of non-Boolean formulas into derivation proofs; our motivation to take square roots is to consider an algebraic system that is at least as strong as Res-Lin even for non-Boolean formulas, see below). Another rule is an algebraic version of Tseitin’s extension rule, which allows us to introduce new variables that are equivalent to arbitrary depth algebraic circuits. We will denote our generalization of Polynomial Calculus as Ext-PC< Note that Ext-PC^ p-simulates Extended Frege system (since Ext- PC^ p-simulates Extended Resolution and Extended Resolution p-simulates Extended Frege [19]), but it’s not obvious how to p-simulate IPS refutations in Ext-PC^ (since IPS refutations polynomials are written as algebraic circuits and Ext-PC^ refutations are written explicitly as a sum of monomials).
In this work we give a partial positive answer to the question raised in [15] asking for a technique for proving size lower bounds on Polynomial Calculus without proving any degree lower bounds. However, our lower bound works only for field Q and the question about proving lower bounds over finite fields remains open. Also, we give a partial answer to another question raised in [15] by proving an exponential lower bound for the system with an extension rule even stronger than that in SHS-PC, which is another extension of Polynomial Calculus presented in the aforementioned work.
We consider the following subset-sum instance, called Binary Value Principle (BVPn) [1, 20]:
1 + xi + 2x2 + ... 2ra-1x„ = 0,
and prove an exponential lower bound for the size of Ext-PCQ refutations of BVPn. Note that Binary Value Principle does not correspond to the translation of any CNF formula and thus the question about proving the size lower bound on the refutation of formulas in CNF without proving degree lower bounds remains open.
Theorem 1.1. Any Ext-PCQ refutation of BVPn requires size 2Q(ra).
The technique we use for proving this lower bound is similar to the technique for proving the conditional IPS lower bound in [1]. However, since Ext-PC proof system is weaker than Ideal Proof System, we get an unconditional lower bound. The main idea of the conditional lower bound in [1] is to prove the complexity lower bound on the free term in the end of the IPS-refutation of BVPn over Z and then show that IPSZ simulates IPSq. One difference is that instead of concentrating on the complexity of computing the free term of the proof, we concentrate on the prime numbers being mentioned in the proof (and thus appearing as factors of the free term).
Then we consider Res-Lin and show that Ext-PCQ simulates Res-Lin and thus get an alternative lower bound for Res-Lin.
Corollary 1.2. Any Res-LinQ refutation of BVPn requires size 2Q(ra).
Note that while Part and Tzameret [20] prove an exponential lower bound on the number of lines in the proof, we prove a bound on the proof size (essentially, on the bit size of scalars appearing in the proof).
1.2 Organization of the paper
In Section 2 we recall the definition of Polynomial Calculus (PC) and give the definitions of Polynomial Calculus with square root (PO^) and Extended Polynomial Calculus with square root (Ext-PC^).
In Section 3 we prove an exponential lower bound on the size of Ext-PCQ refutations of BVPn. We start with considering derivations with integer coefficients (Ext-PCQ) and show that the free term in the end of such refutation of BVPn is not just large but also is divisible by all primes less than 2n (see Theorem 3.1). Then, in Theorem 3.4, we convert proofs over Q into proofs over Z without changing the set of primes mentioned in the proof and thus get an Ext-PCQ lower bound.
In Section 4 we show that Ext-PCQ simulates Res-Lin and thus we get an alternative lower bound for the size of Res-Lin refutations of BVPn.
1.3 Remark about Ext-PC definition
In the original bachelor work, Ext-PC proof system was defined slightly different. The “old” definition allowed us to introduce new variables that encode polynomials depending on the original variables only, which is slightly weaker approach than the present one. However, it turned out that with some modifications, one can use the same technique to prove lower bound for the proof system, in which new variables encode arbitrary algebraic circuits. So, after some discussions with Edward Hirsch, we decided to change the definition of Ext-PC proof system to the present one.
1. Theorem 4.1 says that Ext-PCQ p-simulates any Res-Lin derivation. However, from Theorem 4.3 we know that simulation from Theorem 4.1 does not work for Ext-PCQ. Is the square root rule necessary, that is, can we p-simulate Res-Lin refutations in the Ext-PCQ proof system?
2. A major question is whether it is possible to apply the technique from Section 3 and prove an exponential lower bound on the size of the refutation of a CNF formula.
3. Theorem 4.2 says that any Res-Lin refutation of BVPn requires size 2Q(n). Does the exponential lower bound on the size of the Res-Lin refutation imply the exponential lower bound on the number of lines in the Res-Lin refutation? Do we necessarily need large coefficients in some Res-Lin refutations with a small number of lines? Or is it the case that if there is a Res-Lin refutation with a small number of lines then there is a Res-Lin refutation with a small number of lines and small coefficients?
2. A major question is whether it is possible to apply the technique from Section 3 and prove an exponential lower bound on the size of the refutation of a CNF formula.
3. Theorem 4.2 says that any Res-Lin refutation of BVPn requires size 2Q(n). Does the exponential lower bound on the size of the Res-Lin refutation imply the exponential lower bound on the number of lines in the Res-Lin refutation? Do we necessarily need large coefficients in some Res-Lin refutations with a small number of lines? Or is it the case that if there is a Res-Lin refutation with a small number of lines then there is a Res-Lin refutation with a small number of lines and small coefficients?
Подобные работы
- On scaling entropy for group actions
Дипломные работы, ВКР, математика. Язык работы: Английский. Цена: 4750 р. Год сдачи: 2023