scholarly journals A Tough Nut for Tree Resolution

2000 ◽  
Vol 7 (10) ◽  
Author(s):  
Stefan Dantchev ◽  
Søren Riis
Keyword(s):  
Lower Bound ◽  
Proof Complexity ◽  
Theorem Provers ◽  
Hard Problems ◽  
Tree Resolution

One of the earliest proposed hard problems for theorem provers is<br />a propositional version of the Mutilated Chessboard problem. It is well<br />known from recreational mathematics: Given a chessboard having two<br />diagonally opposite squares removed, prove that it cannot be covered with<br />dominoes. In Proof Complexity, we consider not ordinary, but 2n * 2n<br />mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.

The complexity of analytic tableaux

2006 ◽  
Vol 71 (3) ◽  
pp. 777-790 ◽  
Author(s):  
Noriko H. Arai ◽  
Toniann Pitassi ◽  
Alasdair Urquhart
Keyword(s):  
Lower Bound ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Relative Complexity ◽  
Analytic Tableaux ◽  
Open Questions ◽  
Tree Resolution

AbstractThe method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms of tableaux proofs and also resolve the relative complexity of analytic tableaux versus resolution. We show that there is a quasi-polynomial simulation of tree resolution by analytic tableaux; this simulation is close to optimal, since we give a matching lower bound that is tight to within a polynomial.

Witnessing matrix identities and proof complexity

2018 ◽  
Vol 28 (02) ◽  
pp. 217-256
Author(s):  
Fu Li ◽  
Iddo Tzameret
Keyword(s):  
Computational Complexity ◽  
Lower Bound ◽  
Finite Basis ◽  
Proof Complexity ◽  
Polynomial Identities ◽  
Open Problems ◽  
Complete Proof ◽  
Proof Systems ◽  
Matrix Identity ◽  
Matrix Identities

We use results from the theory of algebras with polynomial identities (PI-algebras) to study the witness complexity of matrix identities. A matrix identity of [Formula: see text] matrices over a field [Formula: see text]is a non-commutative polynomial (f(x1, …, xn)) over [Formula: see text], such that [Formula: see text] vanishes on every [Formula: see text] matrix assignment to its variables. For every field [Formula: see text]of characteristic 0, every [Formula: see text] and every finite basis of [Formula: see text] matrix identities over [Formula: see text], we show there exists a family of matrix identities [Formula: see text], such that each [Formula: see text] has [Formula: see text] variables and requires at least [Formula: see text] many generators to generate, where the generators are substitution instances of elements from the basis. The lower bound argument uses fundamental results from PI-algebras together with a generalization of the arguments in [P. Hrubeš, How much commutativity is needed to prove polynomial identities? Electronic colloquium on computational complexity, ECCC, Report No.: TR11-088, June 2011].We apply this result in algebraic proof complexity, focusing on proof systems for polynomial identities (PI proofs) which operate with algebraic circuits and whose axioms are the polynomial-ring axioms [P. Hrubeš and I. Tzameret, The proof complexity of polynomial identities, in Proc. 24th Annual IEEE Conf. Computational Complexity, CCC 2009, 15–18 July 2009, Paris, France (2009), pp. 41–51; Short proofs for the determinant identities, SIAM J. Comput. 44(2) (2015) 340–383], and their subsystems. We identify a decrease in strength hierarchy of subsystems of PI proofs, in which the [Formula: see text]th level is a sound and complete proof system for proving [Formula: see text] matrix identities (over a given field). For each level [Formula: see text] in the hierarchy, we establish an [Formula: see text] lower bound on the number of proof-steps needed to prove certain identities.Finally, we present several concrete open problems about non-commutative algebraic circuits and speed-ups in proof complexity, whose solution would establish stronger size lower bounds on PI proofs of matrix identities, and beyond.

scholarly journals A Complexity Gap for Tree-Resolution

1999 ◽  
Vol 6 (29) ◽  
Author(s):  
Søren Riis
Keyword(s):  
Predicate Logic ◽  
Proof Complexity ◽  
Polynomial Size ◽  
Combinatorial Principles ◽  
Resolution Proofs ◽  
Symmetrical Group ◽  
Tree Resolution ◽  
Single Proposition ◽  
Exponential Size ◽  
Recent Idea

<p>It is shown that any sequence  psi_n of tautologies which expresses the<br />validity of a fixed combinatorial principle either is "easy" i.e. has polynomial<br />size tree-resolution proofs or is "difficult" i.e requires exponential<br />size tree-resolution proofs. It is shown that the class of tautologies which<br />are hard (for tree-resolution) is identical to the class of tautologies which<br />are based on combinatorial principles which are violated for infinite sets.<br />Actually it is shown that the gap-phenomena is valid for tautologies based<br />on infinite mathematical theories (i.e. not just based on a single proposition).<br />We clarify the link between translating combinatorial principles (or<br />more general statements from predicate logic) and the recent idea of using<br /> the symmetrical group to generate problems of propositional logic.<br />Finally, we show that it is undecidable whether a sequence  psi_n (of the<br />kind we consider) has polynomial size tree-resolution proofs or requires<br />exponential size tree-resolution proofs. Also we show that the degree of<br />the polynomial in the polynomial size (in case it exists) is non-recursive,<br />but semi-decidable.</p><p>Keywords: Logical aspects of Complexity, Propositional proof complexity,<br />Resolution proofs.</p><p> </p>

scholarly journals A lower bound for tree resolution

1994 ◽  
Vol 54 (1) ◽  
pp. 37-53
Author(s):  
David J. McClurkin
Keyword(s):  
Lower Bound ◽  
Tree Resolution

scholarly journals Tabu Search Algorithm Based on Lower Bound and Exact Algorithm Solutions for Minimizing the Makespan in Non-Identical Parallel Machines Scheduling

2021 ◽  
Vol 2021 ◽  
pp. 1-9
Author(s):  
Mohammed A. Noman ◽  
Moath Alatefi ◽  
Abdulrahman M. Al-Ahmari ◽  
Tamer Ali
Keyword(s):  
Lower Bound ◽  
Tabu Search ◽  
Parallel Machines ◽  
Search Algorithm ◽  
Optimal Solution ◽  
Exact Algorithm ◽  
Tabu Search Algorithm ◽  
Scheduling Problems ◽  
Parallel Machines Scheduling ◽  
Hard Problems

Recently, several heuristics have been interested in scheduling problems, especially those that are difficult to solve via traditional methods, and these are called NP-hard problems. As a result, many methods have been proposed to solve the difficult scheduling problems; among those, effective methods are the tabu search algorithm (TS), which is characterized by its high ability to adapt to problems of the large size scale and ease of implementation and gives solution closest to the optimum, but even though those difficult problems are common in many industries, there are only a few numbers of previous studies interested in the scheduling of jobs on unrelated parallel machines. In this paper, a developed TS algorithm based on lower bound (LB) and exact algorithm (EA) solutions is proposed with the objective of minimizing the total completion time (makespan) of jobs on nonidentical parallel machines. The given solution via EA was suggested to enhance and assess the solution obtained from TS. Moreover, the LB algorithm was developed to evaluate the quality of the solution that is supposed to be obtained by the developed TS algorithm and, in addition, to reduce the period for searching for the optimal solution. Two numerical examples from previous studies from the literature have been solved using the developed TS algorithm. Findings show that the developed TS algorithm proved its superiority and speed in giving it the best solution compared to those solutions previously obtained from the literature.

scholarly journals A Reduction based Method for Coloring Very Large Graphs

2017 ◽  
Author(s):  
Jinkun Lin ◽  
Shaowei Cai ◽  
Chuan Luo ◽  
Kaile Su
Keyword(s):  
Lower Bound ◽  
Real World ◽  
Upper Bound ◽  
Practical Importance ◽  
Optimal Solution ◽  
Large Graphs ◽  
Graph Coloring Problem ◽  
Hard Problems ◽  
Novel Method ◽  
Novel Concept

The graph coloring problem (GCP) is one of the most studied NP hard problems and has numerous applications. Despite the practical importance of GCP, there are limited works in solving GCP for very large graphs. This paper explores techniques for solving GCP on very large real world graphs.We first propose a reduction rule for GCP, which is based on a novel concept called degree bounded independent set.The rule is iteratively executed by interleaving between lower bound computation and graph reduction. Based on this rule, we develop a novel method called FastColor, which also exploits fast clique and coloring heuristics. We carry out experiments to compare our method FastColor with two best algorithms for coloring large graphs we could find. Experiments on a broad range of real world large graphs show the superiority of our method. Additionally, our method maintains both upper bound and lower bound on the optimal solution, and thus it proves an optimal solution when the upper bound meets the lower bound. In our experiments, it proves the optimal solution for 97 out of 142 instances.

Logical Foundations of Proof Complexity

2009 ◽  
Author(s):  
Stephen Cook ◽  
Phuong Nguyen
Keyword(s):  
Proof Complexity ◽  
Logical Foundations
Sign in / Sign up

Export Citation Format

Share Document