Mathematical Problems of Computer Science 53, 7–13, 2020. UDC 510.6 Polynomial Bounded Proof Complexities for Some Classes of DNF-Tautologies Garik V. Petrosyan Yerevan State University e-mail: garik.petrosyan.1@gmail.com Abstract In this paper, we present the results on Frege proof complexities of some DNF- tautologies. At first we introduce the notion of complete DNFs and prove that complete DNFs are tautologies, we also show that if the proof complexities for the set of complete DNFs are polynomially bounded, then the set of DNF-tautologies D, for which the number of non-negated variables in every conjunct is O(log(D)), also has polynomially bounded proof complexities. Later we show that the set of all balanced DNF-tautologies has polynomial proof complexities. Keywords: Frege systems, Proof complexity, DNF, complete DNF, balanced for- mulas. 1. Introduction One of the most fundamental problems of the proof complexity theory is to find an efficient proof system for classical propositional calculus. There is a widespread understanding that polynomial-time computability is the correct mathematical model of feasible computation. According to the opinion, a truly ”effective” system should have a polynomial-size p(n) proof for every tautology of size n. In [1], Cook and Reckhow named such a system a super system. They showed that NP = coNP iff there exists a super system. It is well known that many systems are not super. This question about the Frege system, the most natural calculi for propositional logic, is still open. In many papers, some specific sets of tautologies are introduced, and it is shown that the question about polynomially bounded sizes for Frege-proofs of all tautologies is reduced to an analogous question for a set of specific tautologies. In particular, Lutz Strasburger introduced in [2] the notion of balanced formulas and showed that if there are polynomially bounded Frege proofs for the set of balanced tautologies, then the Frege systems are super. An analogous result for some other class of tautologies is proved in [3]. One of the well-known classes of tautologies is the class of tautologies, given in disjunctive normal form (DNF-tautologies), and it is an open question if the Frege-proof complexities for the set of DNF-tautologies have polynomial upper bounds. The Frege-proof complexities of some DNF-tautology classes are investigated in this paper. At first the notion of complete 7 8 Polynomial Bounded Proof Complexities for Some Classes of DNF-Tautologies DNF is introduced, and it is proved that if the proof complexities for the set of complete DNFs are polynomially bounded, then the set of DNF-tautologies D, for which the number of non-negated variables in every conjunct is O(log(D)), also has polynomially bounded proof complexities. Then it is proved that the proof complexities of the set of balanced DNF-tautologies has polynomially bounded proof complexities as well. 2. Main Notions and Notations Here we give basic definitions, which are necessary to give main results. Definition 1: A Frege system F uses a denumerable set of propositional variables, a finite complete set of propositional connectives; F has a finite set of inference rules defined by a figure of the form A1A2...An B (the rules of inference with zero hypotheses are axiom schemes); F must be sound and complete, i.e., for each rule of inference A1A2...An B every truth-value assignment, satisfying A1A2...An, also satisfies B, and F must prove every tautology. The particular choice of a language for the presented propositional formulas is immaterial in this consideration. However, because of some technical reasons, we assume that the language contains the propositional variables pi (i ≥ 1) or pij (i ≥ 1; j ≥ 1) logical connectives ¬,∧,∨,⊃ and parentheses (, ). Note that some parentheses and ∧ can be omitted in generally accepted cases. Note that our convention for serial disjunction A1∨A2∨...∨An (conjunction A1 ∧A2 ∧ ...∧An) associated from left to right. By |ϕ| we denote the size of the formula ϕ defined as the number of all entries of logical signs in it. It is obvious that the full size of the formula, which is understood to be the number of all symbols, is bounded by some linear function in |ϕ|. In the theory of proof complexity, the four main characteristics of the proof are: t- complexity (length), defined as the number of proof steps, l-complexity (size), defined as the sum of sizes for all formulas in the proof (size), s-complexity (space), informally defined as the maximum of minimal sum of sizes for formulas on blackboard needed to verify all steps in the proof (formal definitions are, for example, in [2]) and w-complexity (width), defined as the maximum of sizes of the proof formulas. Definition 2: Let φ be a proof system and ϕ be a tautology. We denote by tφϕ (l φ ϕ, s φ ϕ, w φ ϕ) the minimal possible value of t-complexity (l-complexity, s-complexity, w-complexity) for all -proofs of tautology ϕ. By analogy, we can define the mentioned proof complexity charac- teristics for the proof of any formula A from premises Γ and denote them respectively by t φ Γ`A (l φ Γ`A, s φ Γ`A, w φ Γ`A). Let M be some set of tautologies. Definition 3: We call the φ-proofs of tautologies from the set M t-polynomially (l- polynomially, s-polynomially, w-polynomially) bounded if there is a polynomial p() such that tφϕ ≤ p(|ϕ|) (lφϕ ≤ p(|ϕ|) ,sφϕ ≤ p(|ϕ|) ,wφϕ ≤ p(|ϕ|)) for all tautologies ϕ from M. Note that if φ-proofs of tautologies from the set M are l-polynomially bounded they are also t-polynomially, s-polynomially, w-polynomially bounded. Following the usual terminology, we call the variables and negated variables literals for classical logic. The conjunct K can be represented simply as a set of literals (no conjunct contains a variable and its negation simultaneously). In [4], the notion of balanced formulas is introduced in the following way. G. Petrosyan 9 Definition 4: A propositional formula is called balanced if every variable has only two oc- currences in it, one positive and one with negative. In [4], it is shown that the problem on l-polynomially bounded sizes of proofs for all tau- tologies is reduced to the problem on l-polynomially bounded sizes of proofs for all balanced tautologies. 3. Main Results In this part, Frege-proof complexities for some classes of DNF-tautologies are investigated. A. Here the notion of complete DNF-tautologies is introduced, and it is proved that if the set of complete DNF-tautologies has l-polynomially therefore also t-polynomially, s- polynomially, w-polynomially bounded proofs, then the set of DNF-tautologies D, where the number of non-negated variable in each conjunct is O(log(|D|)), also has l-polynomially therefore also t-polynomially, s-polynomially, w-polynomially bounded proofs. Let all variables of a DNF N1 ∨N2 ∨ ...∨Nn be negated variables. Conjunct K is called representative for D if K contains at least one variable (without negation) from each Ni (1 ≤ i ≤ n), and every variable of K is from D. Definition 5: DNF D1 = C1 ∨ C2 ∨ ... ∨ Cm is called a completion of DNF D2 = N1 ∨ N2 ∨ ...∨Nn iff for every representative K of D2 there is a Ni (1 ≤ i ≤ n), which is a subset of K, and the expression D = (N1 ∨N2 ∨ ...∨Nn)∨(C1 ∨C2 ∨ ...∨Cm) is called a complete DNF. Theorem 1: Complete DNFs are tautologies. Proof. Let’s assume the opposite: there is a complete DNF D = (N1∨N2∨...∨Nn)∨(C1∨ C2∨...∨Cm) such that it is not a tautology. If D = 0 in any collection, then N1∨N2∨...∨Nn should also be 0 in that collection. N1 ∨N2 ∨ ...∨Nn = 0, only if each conjunct is equal to 0, therefore, we have that in each conjunct Ni (1 ≤ i ≤ n) there is a literal equal to 0. If we consider the conjunct P constructed by the conjunction of the variables of these literals, as we have a complete DNF, there is a Cj (1 ≤ j ≤ m) such that Cj is a subset of P , hence Cj = 1, but we have assumed that D = 0, which is a contradiction. From this proof it is easy to see that all DNF-tautologies, the conjuncts of which do not contain a variable and a negated variable simultaneously, are complete DNFs. To evaluate the proof complexities of DNF-tautologies by reducing the proof to the proof of complete DNF- tautologies, we must use some transformations of formulas, therefore we give the following auxiliary statements, which are used to perform those transformations. Lemma 1: For all formulas A,B and C, the set of the following formulas 1. A∨B ⊃ C ≡ (A ⊃ C) ∧ (B ⊃ C) 2. A ⊃ A∨B 3. A ⊃ (B ∨C) ≡ (A ⊃ B) ∨ (A ⊃ C) 4. B ⊃ (A ⊃ A∧B) 5. (A ⊃ B) ⊃ ((A∨C) ⊃ (B ∨C) has l-polynomially bounded proofs. 10 Polynomial Bounded Proof Complexities for Some Classes of DNF-Tautologies Proof. The proof is obvious. Most DNF-tautologies , the proof complexities of which are being investigated, have small conjuncts sizes compered to their size. Using complete DNFs, we can construct polynomial proofs for such DNF-tautologies. The following theorem gives such a construction. Theorem 2: If the set of all complete DNFs has l-polynomially bounded proofs then, the set of DNF-tautologies D, where the number of non-negated variables in each conjunct is O(log(|D|)), also has l-polynomially bounded proofs. Proof. Let’s consider D DNF-tautology, where the number of non-negated variables in each conjunct is O(log(|D|)). For each conjunct, we separate the sub-conjunct of variables with positive entrance and the set of all such conjuncts and its subsets we denote by P . Since the number of non-negated variables in each conjunct is O(log(|D|)), there is such a polynomial p() function that |P| ≤ p(|D|). If DNF is a tautology, it should have at least one conjunct, where all the variables are negated, otherwise it does not cover the 0 point we denote the disjunction of all such conjuncts by N. If D is a tautology, then there is a completion of N such that all conjuncts are from P . If such a completion did not exist, we would take a conjunct constructed by taking one variable from each conjunct of N, and this conjunct would not be covered by P , therefore if we set the values of these variables 1 and the values of all other variables 1, the value of D will be 0. Let’s denote that completion by C. N ∨ C is a completion DNF; to prove D, we need to prove N ∨C and N ∨C ⊃ D, the first part follows from our condition. Let’s prove the second part N ⊃ D. From Lemma 1.1 we get two tautologies to prove N ⊃ D and C ⊃ D. From Lemma 1.2 we get the polynomial proof of N ⊃ D. Now let’s prove C ⊃ D. Suppose C = C1 ∨ C2 ∨ ... ∨ Cm, where Ci(1 ≤ i ≤ m) is a conjunct. Using Lemma 1.1, we can convert C ⊃ D into (C1 ⊃ D) ∧ (C2 ⊃ D) ∧ ...∧ (Cm ⊃ D). As Ci (1 ≤ i ≤ m) is a conjunct, we can prove each one alone and later join them with ∧. Note that the number of such Ci conjuncts is less than P , therefore it has a polynomial upper bound. Using Lemma 1.4 and 5, we can reduce the proof of each (Ci ⊃ D) (1 ≤ i ≤ m) to a new DNF, which also satisfies the condition that the number of non-negated variables in each conjunct is O(log(|D|)). We can use the same technique to prove these new tautologies and note that their P sets are subsets of our initial P set, therefore we will use only the first P . If we continue the proof in this way, we will have several tautologies, the number of which is polynomial from |D|, and each reduction is performed using polynomial steps and polynomial formulas, therefore the proof is l-polynomially bounded. Corollary 3: If the set of complete DNFs has l-polynomially bounded proofs, than the set of DNF-tautologies D, where the number of negated variables in each conjunct is O(log(|D|)), also has l-polynomially bounded proofs. Proof. The proof can be obtained from the proof of Theorem 2 with slight changes. B. Here, the proof complexities of some subset of balanced DNF-tautologies are investigated. Definition 6: A DNF-tautology is correct if DNF, obtained from it by removing any con- junct, is no longer a tautology. Lemma 2: The number of conjuncts in a balanced correct DNF-tautology with n variables is n+1. G. Petrosyan 11 Proof. We prove the lemma by induction on number n of variables in a balanced DNF- tautology D. If n = 1, we have D = ¬p∨p. Suppose the statement is valid for a balanced DNF-tautology, which has ≤ n variables. If the number of variables is n + 1, then the correctly balanced DNF should have at least one conjunct with at least two literals pα1i1 p α2 i2 . After assigning α1 to the variable pi1 everywhere in the given DNF, both the number of variables and the number of conjuncts decrease by one, hence the number of conjuncts in the primary DNF should be n + 2. Corollary 4: Every balanced correct DNF-tautology has at least one conjunct, consisting of one literal. Theorem 5: All balanced correct DNF-tautologies have l-polynomially bounded proofs. Proof. Let us have a balanced correct DNF-tautology D = D1 ∨D2 ∨ ...∨Dn+1, which depends on the variables p1,p2, ...,pn. We take ¬D and prove the a contradiction. ¬D = N1 ∧N2 ∧ ...∧Nn+1, where Ni = ¬Di (1 ≤ i ≤ n + 1) and Ni = pα1i1 ∨p α2 i2 ∨ ...∨pαrir , where αi ∈ {0, 1} (1 ≤ i ≤ n + 1). Based on Ni, we construct the formula Ei by adding instead of every variable pj from p1,p2, ...,pn which has no occurrence in Ni, the formula p1 ∧¬p1 on the j-th place with a disjunction. It is obvious that Ni = Ei, and this equivalence can be derived with polynomially bounded characteristics of proof complexities. By this notation we have that formula ¬D is equivalent to formula D′ = E1 ∧E2...∧En+1. Now we introduce new propositional variables pij (1 ≤ i ≤ n + 1; 1 ≤ j ≤ n), where pij is true if the variable pj occurs in Ni and is false for the opposite case, and construct on the base of Ei new disjunctions D′i by replacing both the primary literals and the formulas p1 ∧¬p1 with the corresponding variables pij. Now we consider the well-known formulas of Pigeon Hole Principle PHPn = ∧ni=0 ∨ n−1 k=0 pik ⊃∨ n−1 k=0 ∨0≤i