scholarly journals Augmenting the Power of (Partial) MaxSat Resolution with Extension

2020 ◽  
Vol 34 (02) ◽  
pp. 1561-1568 ◽  
Author(s):  
Javier Larrosa ◽  
Emma Rollon
Keyword(s):  
Lower Bound ◽  
Objective Function ◽  
Lower Bounds ◽  
Polynomial Time ◽  
Proof System ◽  
Extension Rule ◽  
Resolution Proof

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.

Lower bounds for cutting planes proofs with small coefficients

1997 ◽  
Vol 62 (3) ◽  
pp. 708-728 ◽  
Author(s):  
Maria Bonet ◽  
Toniann Pitassi ◽  
Ran Raz
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Cutting Planes ◽  
Communication Complexity ◽  
Proof System ◽  
Small Weight ◽  
Deduction Rule ◽  
Special Case ◽  
Exponential Lower Bound

AbstractWe consider small-weight Cutting Planes (CP*) proofs; that is, Cutting Planes (CP) proofs with coefficients up to Poly(n). We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP* proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution.We also prove the following two theorems: (1) Tree-like CP* proofs cannot polynomially simulate non-tree-like CP* proofs. (2) Tree-like CP* proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other.Our proofs also work for some generalizations of the CP* proof system. In particular, they work for CP* with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference.

Lower bounds for modal logics

2007 ◽  
Vol 72 (3) ◽  
pp. 941-958 ◽  
Author(s):  
Pavel Hrubeš
Keyword(s):  
Lower Bound ◽  
Modal Logic ◽  
Lower Bounds ◽  
Modal Logics ◽  
Proof System ◽  
Speed Up ◽  
Exponential Lower Bound

AbstractWe give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1, ψ2, … s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4, Gödel–Löb's logic, S andS4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one.

scholarly journals Extended ASP Tableaux and rule redundancy in normal logic programs

2008 ◽  
Vol 8 (5-6) ◽  
pp. 691-716 ◽  
Author(s):  
MATTI JÄRVISALO ◽  
EMILIA OIKARINEN
Keyword(s):  
Answer Set Programming ◽  
Proof System ◽  
Logic Programs ◽  
Interesting Insight ◽  
Extension Rule ◽  
Normal Logic ◽  
Relationship Of ◽  
The Relationship ◽  
Resolution Proof ◽  
Answer Set

AbstractWe introduce an extended tableau calculus for answer set programming (ASP). The proof system is based on the ASP tableaux defined in the work by Gebser and Schaub (Tableau calculi for answer set programming. In Proceedings of the 22nd International Conference on Logic Programming (ICLP 2006), S. Etalle and M. Truszczynski, Eds. Lecture Notes in Computer Science, vol. 4079. Springer, 11–25) with an added extension rule. We investigate the power of Extended ASP Tableaux both theoretically and empirically. We study the relationship of Extended ASP Tableaux with the Extended Resolution proof system defined by Tseitin for sets of clauses, and separate Extended ASP Tableaux from ASP Tableaux by giving a polynomial-length proof for a family of normal logic programs {Φn} for which ASP Tableaux has exponential-length minimal proofs with respect to n. Additionally, Extended ASP Tableaux imply interesting insight into the effect of program simplification on the lengths of proofs in ASP. Closely related to Extended ASP Tableaux, we empirically investigate the effect of redundant rules on the efficiency of ASP solving.

Some classes of concatenated quantum codes: constructions and lower bounds

2015 ◽  
pp. 385-405
Author(s):  
Hachiro Fujita
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Polynomial Time ◽  
Coding Theory ◽  
Minimum Distance ◽  
Concatenated Codes ◽  
Quantum Codes ◽  
Decoding Algorithm ◽  
Quantum Analogue

In classical coding theory code concatenation is successfully used to construct good errorcorrecting codes and most of the asymptotically good codes known so far are based on concatenation. In this paper we present some classes of asymptotically good concatenated quantum codes, which are a quantum analogue of classical concatenated codes, and derive lower bounds on the minimum distance and the rate of the codes. Our bounds improve on the best lower bound of Ashikhmin–Litsyn–Tsfasman and Matsumoto for rates smaller than about one half. We also give a polynomial-time decoding algorithm for the codes that can decode up to one fourth of the lower bound on the minimum distance of the codes.

A Lower Bound for Schur Numbers and Multicolor Ramsey Numbers

10.37236/1188 ◽  
1994 ◽  
Vol 1 (1) ◽  
Author(s):  
Geoffrey Exoo
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Ramsey Numbers

For $k \geq 5$, we establish new lower bounds on the Schur numbers $S(k)$ and on the k-color Ramsey numbers of $K_3$.

scholarly journals A Lower Bound for the Query Phase of Contraction Hierarchies and Hub Labels and a Provably Optimal Instance-Based Schema

Algorithms ◽  
2021 ◽  
Vol 14 (6) ◽  
pp. 164
Author(s):  
Tobias Rupp ◽  
Stefan Funke
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Real World ◽  
Road Network ◽  
Upper And Lower Bounds ◽  
Bounded Degree ◽  
Shortest Path Routing ◽  
Graph Classes ◽  
Speed Up ◽  
To Come

We prove a Ω(n) lower bound on the query time for contraction hierarchies (CH) as well as hub labels, two popular speed-up techniques for shortest path routing. Our construction is based on a graph family not too far from subgraphs that occur in real-world road networks, in particular, it is planar and has a bounded degree. Additionally, we borrow ideas from our lower bound proof to come up with instance-based lower bounds for concrete road network instances of moderate size, reaching up to 96% of an upper bound given by a constructed CH. For a variant of our instance-based schema applied to some special graph classes, we can even show matching upper and lower bounds.

scholarly journals On Computing Multilinear Polynomials Using Multi- r -ic Depth Four Circuits

2021 ◽  
Vol 13 (3) ◽  
pp. 1-21
Author(s):  
Suryajith Chillara
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Complexity Measure ◽  
Natural Question ◽  
Multilinear Polynomial ◽  
Arithmetic Circuit ◽  
Theory Of Computing ◽  
Small Constant ◽  
Multilinear Polynomials ◽  
The Individual

In this article, we are interested in understanding the complexity of computing multilinear polynomials using depth four circuits in which the polynomial computed at every node has a bound on the individual degree of r ≥ 1 with respect to all its variables (referred to as multi- r -ic circuits). The goal of this study is to make progress towards proving superpolynomial lower bounds for general depth four circuits computing multilinear polynomials, by proving better bounds as the value of r increases. Recently, Kayal, Saha and Tavenas (Theory of Computing, 2018) showed that any depth four arithmetic circuit of bounded individual degree r computing an explicit multilinear polynomial on n O (1) variables and degree d must have size at least ( n / r 1.1 ) Ω(√ d / r ) . This bound, however, deteriorates as the value of r increases. It is a natural question to ask if we can prove a bound that does not deteriorate as the value of r increases, or a bound that holds for a larger regime of r . In this article, we prove a lower bound that does not deteriorate with increasing values of r , albeit for a specific instance of d = d ( n ) but for a wider range of r . Formally, for all large enough integers n and a small constant η, we show that there exists an explicit polynomial on n O (1) variables and degree Θ (log 2 n ) such that any depth four circuit of bounded individual degree r ≤ n η must have size at least exp(Ω(log 2 n )). This improvement is obtained by suitably adapting the complexity measure of Kayal et al. (Theory of Computing, 2018). This adaptation of the measure is inspired by the complexity measure used by Kayal et al. (SIAM J. Computing, 2017).

scholarly journals Lower bounds for the state complexity of probabilistic languages and the language of prime numbers

2020 ◽  
Vol 30 (1) ◽  
pp. 175-192
Author(s):  
NathanaËl Fijalkow
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Prime Numbers ◽  
Regular Languages ◽  
Automata Theory ◽  
Seminal Paper ◽  
Probabilistic Automata ◽  
State Complexity ◽  
Probabilistic Languages ◽  
Alternating Automata

Abstract This paper studies the complexity of languages of finite words using automata theory. To go beyond the class of regular languages, we consider infinite automata and the notion of state complexity defined by Karp. Motivated by the seminal paper of Rabin from 1963 introducing probabilistic automata, we study the (deterministic) state complexity of probabilistic languages and prove that probabilistic languages can have arbitrarily high deterministic state complexity. We then look at alternating automata as introduced by Chandra, Kozen and Stockmeyer: such machines run independent computations on the word and gather their answers through boolean combinations. We devise a lower bound technique relying on boundedly generated lattices of languages, and give two applications of this technique. The first is a hierarchy theorem, stating that there are languages of arbitrarily high polynomial alternating state complexity, and the second is a linear lower bound on the alternating state complexity of the prime numbers written in binary. This second result strengthens a result of Hartmanis and Shank from 1968, which implies an exponentially worse lower bound for the same model.

scholarly journals Encoding Two-Dimensional Range Top-k Queries

Algorithmica ◽  
2021 ◽  
Author(s):  
Seungbum Jo ◽  
Rahul Lingala ◽  
Srinivasa Rao Satti
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Upper Bound ◽  
Total Order ◽  
Two Dimensional ◽  
Information Theoretic ◽  
Cartesian Tree ◽  
Dimensional Range

AbstractWe consider the problem of encoding two-dimensional arrays, whose elements come from a total order, for answering $${\text{Top-}}{k}$$ Top- k queries. The aim is to obtain encodings that use space close to the information-theoretic lower bound, which can be constructed efficiently. For an $$m \times n$$ m × n array, with $$m \le n$$ m ≤ n , we first propose an encoding for answering 1-sided $${\textsf {Top}}{\text {-}}k{}$$ Top - k queries, whose query range is restricted to $$[1 \dots m][1 \dots a]$$ [ 1 ⋯ m ] [ 1 ⋯ a ] , for $$1 \le a \le n$$ 1 ≤ a ≤ n . Next, we propose an encoding for answering for the general (4-sided) $${\textsf {Top}}{\text {-}}k{}$$ Top - k queries that takes $$(m\lg {{(k+1)n \atopwithdelims ()n}}+2nm(m-1)+o(n))$$ ( m lg ( k + 1 ) n n + 2 n m ( m - 1 ) + o ( n ) ) bits, which generalizes the joint Cartesian tree of Golin et al. [TCS 2016]. Compared with trivial $$O(nm\lg {n})$$ O ( n m lg n ) -bit encoding, our encoding takes less space when $$m = o(\lg {n})$$ m = o ( lg n ) . In addition to the upper bound results for the encodings, we also give lower bounds on encodings for answering 1 and 4-sided $${\textsf {Top}}{\text {-}}k{}$$ Top - k queries, which show that our upper bound results are almost optimal.

Lower Bounds to the Eigenvalues in One-Dimensional Problems by a Shift in the Weight Function

1970 ◽  
Vol 37 (2) ◽  
pp. 267-270 ◽  
Author(s):  
D. Pnueli
Keyword(s):  
Lower Bound ◽  
Weight Function ◽  
Lower Bounds ◽  
Variational Formulation ◽  
Ritz Method ◽  
The Other ◽  
One Dimensional ◽  
Systematic Shift ◽  
The One ◽  
Detailed Computation

A method is presented to obtain both upper and lower bound to eigenvalues when a variational formulation of the problem exists. The method consists of a systematic shift in the weight function. A detailed procedure is offered for one-dimensional problems, which makes improvement of the bounds possible, and which involves the same order of detailed computation as the Rayleigh-Ritz method. The main contribution of this method is that it yields the “other bound;” i.e., the one which cannot be obtained by the Rayleigh-Ritz method.

Sign in / Sign up

Export Citation Format

Share Document