Abstracts of Selected Publications

Simplified and Improved Separations Between Regular and General Resolution by Lifting

Submitted for publication, 2020

We give a significantly simplified proof of the exponential separation between regular and general resolution of Alekhnovich et al. (2007) as a general theorem lifting proof depth to regular proof length in resolution. This simpler proof then allows us to strengthen the separation further, and to construct families of theoretically very easy benchmarks that are surprisingly hard for SAT solvers in practice.

On Linear Resolution

Journal on Satisfiability, Boolean Modeling and Computation 10, pp. 23-35, 2017.

We discuss the relationship between linear resolution, s-linear resolution and other fragments of resolution, including tree-like resolution, regular resolution and general resolution. We also discuss linear resolution with restarts. We present polynomial-size linear resolution proofs of the ordering tautology, and the guarded ordering tautologies. This shows that regular resolution does not simulate linear resolution.

Available:

Journal page, PDF  

Trade-Offs between Time and Memory in a Tighter Model of CDCL SAT Solvers

in: Nadia Creignou and Daniel LeBerre (eds.), Theory and Applications of Satisfiability Testing, 19th International Conference SAT 2016, Springer LNCS 9710, pp. 160-176, 2016.

A long line of research has studied the power of conflict-driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgotten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that captures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL without any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.

Available:

Springer LNCS page,   PDF  

Backdoors into Two Occurrences

to appear in Journal on Satisfiability, Boolean Modeling and Computation 12, 2020.

Backdoor sets for the class CNF(2) of CNF-formulas in which every variable has at most two occurrences are studied in terms of parameterized complexity. The question whether there exist a CNF(2)-backdoor set size k is hard for the class W[2], for both weak and strong backdoors, and in both cases it becomes fixed-parameter tractable when restricted to inputs in d-CNF for a fixed d. Besides that, it is shown that the problem of finding weak backdoor sets is W[2]-complete, for certain tractable cases. These are the first completeness results in lower levels of the W-hierarchy for any backdoor set problems.

Available:

PDF  

Improved Separations of Regular Resolution from Clause Learning Proof Systems

Journal of Artificial Intelligence Research 49, pp. 669-703, 2014.

This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. This holds even if the CDCL search is required to greedily process conflicts arising from unit propagation. This refutes the conjecture that the guarded graph tautology clauses or the guarded xor-ified pebbling tautology clauses can be used to separate CDCL without restarts from general resolution. Together with subsequent results by Buss and Kolodziejczyk, this means we lack any good conjectures about how to establish the exact logical strength of conflict-driven clause learning without restarts.

Available:

Journal page, PDF  

Exponential Separations in a Hierarchy of Clause Learning Proof Systems

In: Matti Järvisolo and Allen van Gelder (eds.), Theory and Applications of Satisfiability Testing, 16th International Conference SAT 2013, Springer LNCS 7962, pp. 40-51, 2013.

Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments RTL(k) are related to clause learning algorithms where the width of learned clauses is bounded by k. For every k up to O(log n), an exponential separation between the proof systems RTL(k) and RTL(k+1) is shown.

Available:

Springer LNCS page,   PDF  

Lower bounds for width-restricted clause learning on formulas of small width

In: in: Toby Walsh (ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011 Best paper track, pp. 2570-2575, 2011.

Clause learning is a technique used by back\-tracking-based propositional satisfiability solvers, where some clauses obtained by analysis of conflicts are added to the formula during backtracking. It has been observed empirically that clause learning does not significantly improve the performance of a solver when restricted to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from lower bounds on the width of resolution proofs. This yields the first lower bounds on width-restricted clause learning for formulas in 3-CNF.

Available:

PDF  

Lower bounds for width-restricted clause learning on small width formulas

In: Ofer Strichman and Stefan Szeider (eds.), Theory and Applications of Satisfiability Testing, 13th International Conference SAT 2010, Springer LNCS 6175, pp. 16-29, 2010.

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from resolution width lower bounds. This yields the first lower bounds on width-restricted clause learning for formulas in 3-CNF.

Available:

Springer LNCS page,   PDF  

An exponential lower bound for width-restricted clause learning

In: Oliver Kullmann (ed.), Theory and Applications of Satisfiability Testing, 12th International Conference SAT 2009, Springer LNCS 5584, pp. 128-140, 2009.

It has been observed empirically that clause learning does not significantly improve the performance of a satisfiably solver when restricted to learning short clauses only. This experience is supported by a lower bound theorem: an unsatisfiable set of clauses, claiming the existence of an ordering of n points without a maximum element, can be solved in polynomial time when learning arbitrary clauses, but it is shown to require exponential time when learning only clauses of size at most n/4. The lower bound is of the same order of magnitude as a known lower bound for backtracking algorithms without any clause learning. It is shown by proving lower bounds on the proof length in a certain resolution proof system related to clause learning.

Available:

Springer LNCS page,   PDF  

Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL-Algorithms with Clause Learning

Logical Methods in Computer Science 4 (4:13), 2008 .

Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regular proofs, an exponential separation between regular dag-like resolution and both regular WRTL and regular WRTI is given.

It is proved that DLL proof search algorithms that use clause learning based on unit propagation can be polynomially simulated by regular WRTI. More generally, non-greedy DLL algorithms with learning by unit propagation are equivalent to regular WRTI. A general form of clause learning, called DLL-Learn, is defined that is equivalent to regular WRTL.

A variable extension method is used to give simulations of resolution by regular WRTI, using a simplified form of proof trace extensions. DLL-Learn and non-greedy DLL algorithms with learning by unit propagation can use variable extensions to simulate general resolution without doing restarts.

Finally, an exponential lower bound for WRTL where the lemmas are restricted to short clauses is shown.

Available:

Journal page   PDF

Optimal lower bounds on regular expression size using communication complexity

In: Roberto Amadio (ed.): Foundations of Software Science and Computational Structures, 11th Intl. Conference FOSSACS 2008, Springer LNCS 4962, pp. 273-286, 2008.

The problem of converting deterministic finite automata into (short) regular expressions is considered. It is known that the required expression size is 2^Θ(n) in the worst case for infinite languages, and for finite languages it is n^{Ω(log log n)} and n^{O(log n)}, if the alphabet size grows with the number of states n of the given automaton. A new lower bound method based on communication complexity for regular expression size is developed to show that the required size is indeed n^{Θ(log n)}.

For constant alphabet size the best lower bound known to date is Ω(n²), even when allowing infinite languages and nondeterministic finite automata. As the technique developed here works equally well for deterministic finite automata over binary alphabets, the lower bound is improved to n^{Ω(log n)}.

Available:

Springer LNCS page,   PDF

Bounded model checking for all regular properties

Proceedings of the third International Workshop on Bounded Model Checking (BMC 2005), Electronic Notes in Theoretical Computer Science 144 no. 1, pp. 1-92.

Bounded Model Checking is a successful approximation technique for model checking the linear time temporal logic LTL. But the expressive power of LTL is rather limited: it can only express First-Order-definable properties on omega-words. In order to be able to express Monadic-Second-Order-, i.e., regular properties of infinite words, one can employ the linear time mu-calculus. This paper shows how to extend the technique of bounded model checking to this logic.

Available:

ENTCS page, PDF

The complexity of pure literal elimination

Journal of Automated Reasoning 35 No. 1-3, special issue on SAT 2005, pp. 88-95 (2005)

The complexity of eliminating pure literals from CNF formulas is classified for several classes of formulas. In general, the problem is P-complete, for 2-CNF formulas it is NL-complete, and for formulas with at most two occurrences of every variable it is SL-complete.

Available:

Journal page, PDF

An unexpected separation result in linearly bounded arithmetic

Mathematical Logic Quarterly 51, no.2, pp. 191-200 (2005).

The theories Sⁱ₁(α) and Tⁱ₁(α) are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σ^b_i+1(α)-formula TOPⁱ(α), which expresses a form of the total ordering principle, is exhibited that is provable in Sⁱ⁺¹₁(α), but unprovable in Tⁱ₁(α). This is in contrast with the classical situation, where Sⁱ⁺¹₂ is conservative over Tⁱ₂w.r.t. Σ^b_i+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems.

Available:

Journal page   PDF

Satisfiability problems complete for deterministic logarithmic space

In: Volker Diekert and Michel Habib (eds.): STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. Springer LNCS 2996, pp. 317-325, 2004.

The satisfiability and not-all-equal satisfiability problems for boolean formulas in CNF with at most two occurrences of each variable are complete for deterministic logarithmic space.

Available:

Springer LNCS page,   PDF

CTL⁺ is complete for double exponential time

In: J. C. M. Baeten et al., editors, Proc. 30th Int. Coll. on Automata, Logics and Programming (ICALP'03), Springer LNCS 2719, pp. 767-775, 2003.

We show that the satisfiability problem for CTL⁺, the branching time logic that allows boolean combinations of path formulas inside a path quantifier but no nesting of them, is 2-EXPTIME-hard. The construction is inspired by Vardi and Stockmeyer's 2-EXPTIME-hardness proof of CTL*'s satisfiability problem. As a consequence, there is no subexponential reduction from CTL⁺ to CTL which preserves satisfiability.

Available:

Springer LNCS page,   PDF

An Optimal Lower Bound for Resolution with 2-Conjunctions

Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS) Springer LNCS 2420, pp. 387-398

A lower bound is proved for refutations of certain clause sets in a generalization of Resolution that allows cuts on conjunctions of width 2. The hard clauses are the Tseitin graph formulas for a class of logarithmic degree expander graphs. The bound is optimal in the sense that it is truly exponential in the number of variables.

Note: the proof in the paper is wrong. We have a corrected proof that gives a slightly weaker lower bound of exp(N/log N) where N is the number of variables. This proof is not written up in digital form.

Available:

Springer LNCS page  

An Exponential Separation between Regular and General Resolution

Theory of Computing 3 article 5, pp. 81 - 102. Preliminary versions appeared in Proceedings of the 34th ACM Symposium on Theory of Computing (STOC 2002), and as Electronic Colloquium on Computational Complexity TR 01-56, 2001.

This paper gives two distinct proofs of an exponential separation between regular resolution and unrestricted resolution. The previous best known separation between these systems was quasi-polynomial.

Available:

TOC page,   ACM DL page (STOC version),  ECCC

An Elementary Fragment of Second-Order Lambda Calculus

ACM Transactions on Computational Logic 6 no.2, pp. 468 - 480. Preliminary version available on CoRR as cs.LO/0210022

A fragment of second-order lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be non-interleaved and stratified, i.e., the types are assigned levels, and a quantified variable can only be instantiated by a type of smaller level, with a slightly liberalized treatment of the level zero.

Available:

Journal page,  CoRR page,  PDF

Linear Ramified Higher Type Recursion and Parallel Complexity

in: R. Kahle, P. Schröder-Heister, R. Stärk (eds.) "Proof Theory in Computer Science", Springer LNCS 2183, 2001

A typed lambda calculus with recursion in all finite types is defined such that the first order terms exactly characterize the parallel complexity class NC. This is achieved by use of the appropriate forms of recursion (concatenation recursion and logarithmic recursion), a ramified type structure and imposing of a linearity constraint.

Available:

Springer LNCS page,   PDF

Depth Lower Bounds for Monotone Semi-Unbounded Fan-In Circuits

RAIRO Theoretical Informatics and Applications 35(3) pp. 277-286, 2001

The depth hierarchy results for monotone circuits of Raz and McKenzie (Combinatorica 19, 1999) are extended to the case of monotone circuits of semi-unbounded fan-in. It follows that the inclusions NCⁱ <= SACⁱ <= ACⁱ are proper in the monotone setting, for every i>=1.

Available:

Journal page   PDF

Cumulative Higher-Order Logic as a Foundation for Set Theory

Mathematical Logic Quarterly 46 (2000) pp. 147-170

The systems $K_\alpha$ of transfinite cumulative types up to $\alpha$ are extended to systems $K_\alpha^\infty$ that include a natural infinitary inference rule, the so-called limit rule. For countable $\alpha$ a semantic completeness theorem for $K_\alpha^\infty$ is proved by the method of reduction trees, and it is shown that every model of $K_\alpha^\infty$ is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic first-order set theories can be interpreted in $K_\alpha^\infty$, for suitable $\alpha$.

Available:

Journal page   PDF

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems

SIAM Journal on Computing, Vol. 30, No. 5 (2000), pp. 1462-1484

An exponential lower bound for the size of tree-like Cutting Planes refutations of a certain family of CNF formulas with polynomial size resolution refutations is proved. This implies an exponential separation between the tree-like versions and the dag-like versions of resolution and Cutting Planes. In both cases only superpolynomial separations were known. In order to prove these separations, the lower bounds on the depth of monotone circuits of Raz and McKenzie (FOCS 97) are extended to monotone real circuits.

An exponential separation is also proved between tree-like resolution and several refinements of resolution: negative resolution and regular resolution. Actually this last separation also provides a separation between tree-like resolution and ordered resolution, thus the corresponding superpolynomial separation of Urquhart (Bull. Symb. Logic 1, 1995) is extended.

Finally, an exponential separation between ordered resolution and unrestricted resolution (also negative resolution) is proved. Only a superpolynomial separation between ordered and unrestricted resolution was previously known (Goerdt, Ann. Math. Artificial Intelligence 6, 1992).

Available:

Journal page   PDF

On the Δ^b₁-Bit-Comprehension Rule

In: S. Buss, P. Hájek, P. Pudlák (eds.) "Logic Colloquium '98", ASL Lecture Notes in Logic, 2000

The theory Δ^b₁-CR of Bounded Arithmetic axiomatized by the Δ^b₁-bit-comprehension rule is defined and shown to be strongly related to the complexity class TC⁰. The Σ^b₁-definable functions of Δ^b₁-CR are those in uniform TC⁰, and the Σ^b₂-definable functions are computable by counterexample computations using TC⁰-functions. The latter is used to show that a collapse of stronger theories to Δ^b₁-CR implies that NP is contained in non-uniform TC⁰.

Available:

PDF

Weak Bounded Arithmetic, the Diffie-Hellman Problem, and Constable's Class K

Proceedings of the 14th IEEE Symposium on Logic in Computer Science, Trento, Italy, 1999

The bounded arithmetic theory $C^0_2$ of Johannsen and Pollett (1998), which is closely related to the complexity class DLogTime-uniform $TC^0$, is extended by a function symbol and axioms for integer division, which is not known to be in DLogTime-uniform $TC^0$. About this extended theory $C^0_2[div]$, two main results are proved:

1. The $\Sigma^b_1$-definable functions of $C^0_2[div]$ are exactly Constable's class $K$, a function algebra whose precise complexity-theoretic nature is yet to be determined. This also yields the new upper bound $K \subseteq$ uniform $NC^2$.

2. The $\Delta^b_1$-theorems of $C^0_2[div]$ do not have Craig-interpolants of polynomial circuit size, unless the Diffie-Hellman key exchange protocol is insecure.

Available:

IEEE page,   PDF

A Remark on Independence Results for Sharply Bounded Arithmetic

Mathematical Logic Quarterly 44(4) pp. 568-570, 1998

The purpose of this note is to show that the independence results for sharply bounded arithmetic of Takeuti (Contemp. Math. 106, 1990) and Tada and Tatsuta (Arch. Math. Logic 37, 1997) can be obtained and, in case of the latter, improved by the model-theoretic method developed by the author in his thesis and (MLQ 44(2), 1998).

Available:

Journal page  

On Proofs about Threshold Circuits and Counting Hierarchies (Extended Abstract)

Proceedings of the 13th IEEE Symposium on Logic in Computer Science, Indianapolis, 1998

We define theories of Bounded Arithmetic characterizing classes of functions computable by constant-depth threshold circuits of polynomial and quasi-polynomial size. Then we define certain second-order theories and show that they characterize the functions in the Counting Hierarchy. Finally we show that the former theories are isomorphic to the latter via the so-called RSUV-isomorphism.

Available:

IEEE page,   PDF

Equational Calculi and Constant-Depth Propositional Proofs

In: P. Beame, S. Buss (eds.) "Proof Complexity and Feasible Arithmetic", AMS DIMACS Series Vol. 39, 1998

We define equational calculi for proving equations between functions in the complexity classes ACC(2) and TC^0, and we show that proofs in these calculi can be simulated by polynomial size, constant depth proofs in Frege systems with counting modulo 2 and threshold connectives respectively.

Available:

PDF

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

Proceedings of the 39th IEEE Symposium on Foundations of Computer Science, Palo Alto, 1998

An exponential lower bound is proved for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both Cutting Planes and resolution; in both cases only superpolynomial separations were known before. In order to prove this, the lower bounds on the depth of monotone circuits of Raz and McKenzie (FOCS 1997) are extended to monotone real circuits.

In the case of resolution, this result is further improved by giving an exponential separation of tree-like resolution from (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Putnam resolution proof. This extends the corresponding superpolynomial separation of Urquhart (Bull. Symb. Logic 1, 1995).

Finally, an exponential separation is proved between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known from Goerdt (Ann. Math. Artificial Intelligence 6, 1992).

Available:

IEEE page   PDF

A Model-Theoretic Property of Sharply Bounded Formulae, with some Applications

Mathematical Logic Quarterly 44(2) pp. 205-215, 1998

We define a property of substructures of models of arithmetic, that of being length-initial, and show that sharply bounded formulae are absolute between a model and its length-initial submodels. We use this to prove independence results for some weak fragments of bounded arithmetic by constructing appropriate models as length-initial submodels of some given model.

Available:

Journal page   PDF

Lower Bounds for Monotone Real Circuit Depth and Formula Size and Tree-like Cutting Planes

Information Procesing Letters 67 (1) pp. 37-41, 1998

Using a notion of real communication complexity recently introduced by J. Krajicek, we prove a lower bound on the depth of monotone real circuits and the size of monotone real formulas for st-connectivity. This implies a super-polynomial speed-up of dag-like over tree-like Cutting Planes proofs.

Available:

Journal page   PDF

A Bounded Aritmetic Theory for Constant-Depth Threshold Circuits

In: P. Hájjek (ed.) "GÖDEL '96", Lecture Notes in Logic 6, pp. 224-234, 1996

We define an extension \bar{R}^0_2 of the bounded arithmetic theory R^0_2 and show that the class of functions \Sigma^b_1-definable in \bar{R}^0_2 coincides with the computational complexity class TC^0 of functions computable by polynomial size, constant-depth threshold circuits.

Available:

CUP Lecture Notes in Logic page, PDF

On Sharply Bounded Length Induction

In: Proc. of Computer Science Logic '95, Paderborn 1995, Springer LNCS 1092, 1996

We construct models of the theory L_2^0 := BASIC + \Sigma^b_0-LIND: one where the predecessor function is not total and one not satisfying \Sigma^b_0-PIND, showing that L_2^0 is strictly weaker that S_2^0. The construction also shows that S_2^0 is not \forall\Sigma^b_0-axiomatizable.

Available:

Springer LNCS page,   PDF

A Note on Sharply Bounded Arithmetic

Archive for Mathematical Logic 33 pp. 159-165, 1994

We prove some independence results for the bounded arithmetic theory R^0_2, and we define a class of functions that is shown to be an upper bound for the class of functions definable by a certain restricted class of \Sigma^b_1-formulae in extensions of R^0_2.

Available:

Journal page,   PDF

On the Weakness of Sharply Bounded Polynomial Induction

In: G. Gottlob et al. (eds.) "Computational Logic and Proof Theory", Proceedings of KGC'93, Brno 1993, Springer LNCS 713, pp. 223-230, 1993

We shall show that if the theory S^0_2 of sharply bounded polynomial induction is extended by symbols for certain functions and their defining axioms, it is still far weaker than T^0_2, which has ordinary sharply bounded induction. Furthermore, we show that this extended system S^0_{2^+} cannot \Sigma^b_1-define every function in AC^0, the class of functions computable by polynomial size constant depth circuits.

Available:

Springer LNCS page,   PDF

Home Page          TCS          Computer Science Institute          University