-
The strength of the dominance rule
Authors:
Leszek Aleksander Kołodziejczyk,
Neil Thapen
Abstract:
It has become standard that, when a SAT solver decides that a CNF $Γ$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $Γ$ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023]…
▽ More
It has become standard that, when a SAT solver decides that a CNF $Γ$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $Γ$ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system $G_1$, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.
△ Less
Submitted 19 June, 2024;
originally announced June 2024.
-
Notes on switching lemmas
Authors:
Neil Thapen
Abstract:
We prove three switching lemmas, for random restrictions for which variables are set independently; for random restrictions where variables are set in blocks (both due to Hastad [Hastad 86]); and for a distribution appropriate for the bijective pigeonhole principle [Beame et al. 94, Krajicek et al. 95]. The proofs are based on Beame's version [Beame 94] of Razborov's proof of the switching lemma i…
▽ More
We prove three switching lemmas, for random restrictions for which variables are set independently; for random restrictions where variables are set in blocks (both due to Hastad [Hastad 86]); and for a distribution appropriate for the bijective pigeonhole principle [Beame et al. 94, Krajicek et al. 95]. The proofs are based on Beame's version [Beame 94] of Razborov's proof of the switching lemma in [Razborov 93], except using families of weighted restrictions rather than families of restrictions which are all the same size. This follows a suggestion of Beame in [Beame 94]. The result is something between Hastad's and Razborov's methods of proof. We use probabilistic arguments rather than counting ones, in a similar way to Hastad, but rather than doing induction on the terms in our formula with an inductive hypothesis involving conditional probability, as Hastad does, we explicitly build one function to bound the probabilities for the whole formula.
△ Less
Submitted 11 February, 2022;
originally announced February 2022.
-
First-Order Reasoning and Efficient Semi-Algebraic Proofs
Authors:
Fedor Part,
Neil Thapen,
Iddo Tzameret
Abstract:
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS p…
▽ More
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds.
This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones.
We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.
△ Less
Submitted 18 May, 2021; v1 submitted 16 May, 2021;
originally announced May 2021.
-
DRAT and Propagation Redundancy Proofs Without New Variables
Authors:
Sam Buss,
Neil Thapen
Abstract:
We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $Γ$ derive the set of clauses $Γ\cup \{ C \}$ where, due to some syntactic condition, $Γ\cup \{ C \}$ is satisfiable if $Γ$ is, but where $Γ$ does not necessarily imply $C$. These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolu…
▽ More
We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $Γ$ derive the set of clauses $Γ\cup \{ C \}$ where, due to some syntactic condition, $Γ\cup \{ C \}$ is satisfiable if $Γ$ is, but where $Γ$ does not necessarily imply $C$. These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolution asymmetric tautologies, subset propagation redundancy and propagation redundancy), which arose from work in satisfiability (SAT) solving. We introduce a new, more general rule SR (substitution redundancy).
If the new clause $C$ is allowed to include new variables then the systems based on these rules are all equivalent to extended resolution. We focus on restricted systems that do not allow new variables. The systems with deletion, where we can delete a clause from our set at any time, are denoted DBC${}^-$, DRAT${}^-$, DSPR${}^-$, DPR${}^-$ and DSR${}^-$. The systems without deletion are BC${}^-$, RAT${}^-$, SPR${}^-$, PR${}^-$ and SR${}^-$.
With deletion, we show that DRAT${}^-$, DSPR${}^-$ and DPR${}^-$ are equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC${}^-$. Without deletion, we show that SPR${}^-$ can simulate PR${}^-$ provided only short clauses are inferred by SPR inferences. We also show that many of the well-known "hard" principles have small SPR${}^-$ refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR${}^-$ can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower bound for RAT${}^-$ refutations, giving exponential separations between RAT${}^-$ and both DRAT${}^-$ and SPR${}^-$.
△ Less
Submitted 22 April, 2021; v1 submitted 1 September, 2019;
originally announced September 2019.
-
Approximate counting and NP search problems
Authors:
Leszek Aleksander Kołodziejczyk,
Neil Thapen
Abstract:
We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory $\mathrm{APC}_2$ of [Jeřábek 2009]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class an…
▽ More
We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory $\mathrm{APC}_2$ of [Jeřábek 2009]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS.
As CPLS is provably total in the theory $T^2_2$, this shows that $\mathrm{APC}_2$ does not prove every $\forall Σ^b_1$ sentence which is provable in bounded arithmetic. This answers the question posed in [Buss, Kołodziejczyk, Thapen 2014] and represents some progress in the programme of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences.
Our main technical tool is an extension of the "fixing lemma" from [Pudlák, Thapen 2017], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a $\textrm{P}^{\textrm{NP}}$ oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic.
△ Less
Submitted 26 November, 2021; v1 submitted 27 December, 2018;
originally announced December 2018.
-
DEFENDER: Detecting and Forecasting Epidemics using Novel Data-analytics for Enhanced Response
Authors:
Donal Simmie,
Nicholas Thapen,
Chris Hankin
Abstract:
In recent years social and news media have increasingly been used to explain patterns in disease activity and progression. Social media data, principally from the Twitter network, has been shown to correlate well with official disease case counts. This fact has been exploited to provide advance warning of outbreak detection, tracking of disease levels and the ability to predict the likelihood of i…
▽ More
In recent years social and news media have increasingly been used to explain patterns in disease activity and progression. Social media data, principally from the Twitter network, has been shown to correlate well with official disease case counts. This fact has been exploited to provide advance warning of outbreak detection, tracking of disease levels and the ability to predict the likelihood of individuals develo** symptoms. In this paper we introduce DEFENDER, a software system that integrates data from social and news media and incorporates algorithms for outbreak detection, situational awareness, syndromic case tracking and forecasting. As part of this system we have developed a technique for creating a location network for any country or region based purely on Twitter data. We also present a disease count tracking approach which leverages counts from multiple symptoms, which was found to improve the tracking of diseases by 37 percent over a model that used only previous case data. Finally we attempt to forecast future levels of symptom activity based on observed user movement on Twitter, finding a moderate gain of 5 percent over a time series forecasting model.
△ Less
Submitted 16 April, 2015;
originally announced April 2015.
-
The Early Bird Catches The Term: Combining Twitter and News Data For Event Detection and Situational Awareness
Authors:
Nicholas Thapen,
Donal Simmie,
Chris Hankin
Abstract:
Twitter updates now represent an enormous stream of information originating from a wide variety of formal and informal sources, much of which is relevant to real-world events. In this paper we adapt existing bio-surveillance algorithms to detect localised spikes in Twitter activity corresponding to real events with a high level of confidence. We then develop a methodology to automatically summaris…
▽ More
Twitter updates now represent an enormous stream of information originating from a wide variety of formal and informal sources, much of which is relevant to real-world events. In this paper we adapt existing bio-surveillance algorithms to detect localised spikes in Twitter activity corresponding to real events with a high level of confidence. We then develop a methodology to automatically summarise these events, both by providing the tweets which fully describe the event and by linking to highly relevant news articles. We apply our methods to outbreaks of illness and events strongly affecting sentiment. In both case studies we are able to detect events verifiable by third party sources and produce high quality summaries.
△ Less
Submitted 9 April, 2015;
originally announced April 2015.
-
The complexity of proving that a graph is Ramsey
Authors:
Massimo Lauria,
Pavel Pudlák,
Vojtěch Rödl,
Neil Thapen
Abstract:
We 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 s…
▽ More
We 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.
△ Less
Submitted 13 March, 2013;
originally announced March 2013.
-
The strength of replacement in weak arithmetic
Authors:
Stephen Cook,
Neil Thapen
Abstract:
The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption.
The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption.
△ Less
Submitted 8 September, 2004;
originally announced September 2004.
