1,720,980 research outputs found
On semantic cutting planes with very small coefficients
No full textCutting planes proofs for integer programs can naturally be defined both in a syntactic and in a semantic fashion. Filmus et al. (STACS 2016) proved that semantic cutting planes proofs may be exponentially stronger than syntactic ones, even if they use the semantic rule only once. We show that when semantic cutting planes proofs are restricted to have coefficients bounded by a function growing slowly enough, syntactic cutting planes can simulate them efficiently. Furthermore if we strengthen the restriction to a constant bound, then the simulating syntactic proof even has polynomially small coefficients
Total space in resolution
No full textWe show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the open problem of whether there are families of k-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large widt
The complexity of proving that a graph is Ramsey
No full textWe say that a graph with n vertices is c-Ramsey if it does not contain either a clique or an independent set of size clogn. We define a CNF formula which expresses this property for a graph G. We show a superpolynomial lower bound on the length of resolution proofs that G is c-Ramsey, for every graph G. Our proof makes use of the fact that every Ramsey graph must contain a large subgraph with some of the statistical properties of the random graph
The complexity of proving that a graph is Ramsey
No full textWe say that a graph with n vertices is c-Ramsey if it does not contain either a clique or an independent set of size c log n. We define a CNF formula which expresses this property for a graph G. We show a superpolynomial lower bound on the length of resolution proofs that G is c-Ramsey, for every graph G. Our proof makes use of the fact that every Ramsey graph must contain a large subgraph with some of the statistical properties of the random graph.</p
The Space Complexity of Cutting Planes Refutations
Full text linkWe study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known.
Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle.
We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols
Logika a kryptografie
Full text linkTitle: Logic and cryptography Author: Bc.Vojtěch Wagner Department: Department of Algebra Supervisor: prof. RNDr. Jan Krajíček, DrSc. Abstract: This work is devoted to a study of a formal method of formalization of cryptographic constructions. It is based on defining a multi-sorted formal logic theory T composed of strings, integers and objects of sort k - k-ary functions. We allow some operations on them, formulate axioms, terms and formulas. We also have a special type of integers called the counting integers. It denotes the number of x from a given interval satisfying formula ϕ(x). It allows us to talk about probabilities and use terms of probability theory. The work first describes this theory and then it brings a formalization of the Goldreich-Levin theorem. The goal of this work is to adapt all needed cryptographic terms into the language of T and then prove the theorem using objects, rules and axioms of T. Presented definitions and principles are ilustrated on examples. The purpose of this work is to show that such theory is sufficiently strong to prove such cryptographic constructions and verify its correctness and security. Keywords: cryptography, protocol verifying, Soundness theorem, formal logic theory, the Goldreich-Levin theorem
Model constructions for bounded arithmetic
No full textTitle: Model constructions for bounded arithmetic Author: Michal Garlík Abstract: We study constructions of models of bounded arithmetic theories. Us- ing basic techniques of model theory we give a new proof of Ajtai's completeness theorem for nonstandard finite structures. Working in the framework of restricted reduced powers (a generalization of the ultrapower construction) we devise two methods of constructing models of bounded arithmetic. The first one gives a new proof of Buss's witnessing theorem. Using the second method we show that the theory R1 2 is stronger than its variant strictR1 2 under a plausible computational assumption (the existence of a strong enough one-way permutation), and that the theory PV1 + Σb 1(PV ) − LLIND is stronger than PV1 + strictΣb 1(PV ) − LLIND under the same assumption. Considering relativized theories, we show that R1 2(α) is stronger than strictR1 2(α) (unconditionally).
On the Power of Weak Extensions of V0
No full textNázev práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra...
The BSS model and cryptography
No full textReal numbers are usually represented by various discrete objects such as floating points or partial decimal expansions. This is mainly because the clas- sical computability theory relates to computers which work with discrete data. Nevertheless, for theoretical purposes it is interesting to look at models of com- putation that deal with real numbers as with objects of unit size. A very natural such model was suggested by Blum, Shub and Smale in 1989. In 2012 Grigoriev and Nikolenko studied various cryptographic tasks involv- ing real numbers (for example, biometric authentication) and they considered the BSS machine model. In this work we focus on hard to invert functions in this model of computation. Our main theme is to analyse whether there are real functions of one variable that are easier to compute than to invert by a BSS machine.
- …
