Abstracts
Abstracts of Selected Publications
Simplified and Improved Separations Between Regular and General Resolution by Lifting
Marc Vinyals, Jan Elffers, Jan Johannsen and Jakob Nordström
in: Luca Pulina and Martina Seidl (eds.), Theory and Applications of Satisfiability Testing, 23rd International Conference SAT 2020, Springer LNCS 12178, pp. 182200, 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
Samuel R. Buss and Jan Johannsen
Journal on Satisfiability, Boolean Modeling and Computation 10, pp. 2335, 2017.
We discuss the relationship between linear resolution, slinear resolution and other fragments of resolution, including treelike resolution, regular resolution and general resolution. We also discuss linear resolution with restarts. We present polynomialsize linear resolution proofs of the ordering tautology, and the guarded ordering tautologies. This shows that regular resolution does not simulate linear resolution.
TradeOffs between Time and Memory in a Tighter Model of CDCL SAT Solvers
Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström and Marc Vinyals
in: Nadia Creignou and Daniel LeBerre (eds.), Theory and Applications of Satisfiability Testing, 19th International Conference SAT 2016, Springer LNCS 9710, pp. 160176, 2016.
A long line of research has studied the power of conflictdriven 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 blowup 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 finegrained model of CDCL that captures not only time but also memory usage and number of restarts. We show how previously established strong sizespace tradeoffs for resolution can be transformed into equally strong tradeoffs 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.
Backdoors into Two Occurrences
Journal on Satisfiability, Boolean Modeling and Computation 12, No. 1, pp. 115, 2020.
Backdoor sets for the class CNF(2) of CNFformulas 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 fixedparameter tractable when restricted to inputs in dCNF 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 Whierarchy for any backdoor set problems.
 Journal page, PDF

Improved Separations of Regular Resolution from Clause Learning Proof Systems
Maria Luisa Bonet, Samuel R. Buss and Jan JohannsenJournal of Artificial Intelligence Research 49, pp. 669703, 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, xorified 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 xorified 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 conflictdriven clause learning without restarts.
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. 4051, 2013.
Resolution trees with lemmas (RTL) are a resolutionbased 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.
Lower bounds for widthrestricted clause learning on formulas of small width
Eli BenSasson and Jan Johannsen
In: in: Toby Walsh (ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011 Best paper track, pp. 25702575, 2011.
Clause learning is a technique used by backtrackingbased 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 widthrestricted clause learning follow from lower bounds on the width of resolution proofs. This yields the first lower bounds on widthrestricted clause learning for formulas in 3CNF.
Lower bounds for widthrestricted clause learning on small width formulas
Eli BenSasson and Jan Johannsen
In: Ofer Strichman and Stefan Szeider (eds.), Theory and Applications of Satisfiability Testing, 13th International Conference SAT 2010, Springer LNCS 6175, pp. 1629, 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 widthrestricted clause learning follow from resolution width lower bounds. This yields the first lower bounds on widthrestricted clause learning for formulas in 3CNF.
An exponential lower bound for widthrestricted clause learning
In: Oliver Kullmann (ed.), Theory and Applications of Satisfiability Testing, 12th International Conference SAT 2009, Springer LNCS 5584, pp. 128140, 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.
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLLAlgorithms with Clause Learning
Samuel R. Buss, Jan Hoffmann and Jan Johannsen.
Logical Methods in Computer Science 4 (4:13), 2008 .
Resolution refinements called wresolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Daglike resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regular proofs, an exponential separation between regular daglike 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, nongreedy DLL algorithms with learning by unit propagation are equivalent to regular WRTI. A general form of clause learning, called DLLLearn, 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. DLLLearn and nongreedy 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.
 Journal page PDF

Optimal lower bounds on regular expression size using communication complexity
Hermann Gruber and Jan Johannsen.In: Roberto Amadio (ed.): Foundations of Software Science and Computational Structures, 11th Intl. Conference FOSSACS 2008, Springer LNCS 4962, pp. 273286, 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^{2}), 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)}.
 Springer LNCS page, PDF

Bounded model checking for all regular properties
Markus Jehle, Jan Johannsen, Martin Lange and Nicolas RachinskyProceedings of the third International Workshop on Bounded Model Checking (BMC 2005), Electronic Notes in Theoretical Computer Science 144 no. 1, pp. 192.
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 FirstOrderdefinable properties on omegawords. In order to be able to express MonadicSecondOrder, i.e., regular properties of infinite words, one can employ the linear time mucalculus. This paper shows how to extend the technique of bounded model checking to this logic.
 ENTCS page, PDF

The complexity of pure literal elimination
Jan JohannsenJournal of Automated Reasoning 35 No. 13, special issue on SAT 2005, pp. 8895 (2005)
The complexity of eliminating pure literals from CNF formulas is classified for several classes of formulas. In general, the problem is Pcomplete, for 2CNF formulas it is NLcomplete, and for formulas with at most two occurrences of every variable it is SLcomplete.
 Journal page, PDF

An unexpected separation result in linearly bounded arithmetic
Arnold Beckmann and Jan JohannsenMathematical Logic Quarterly 51, no.2, pp. 191200 (2005).
The theories S^{i}_{1}(α) and T^{i}_{1}(α) 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^{i}(α), which expresses a form of the total ordering principle, is exhibited that is provable in S^{i+1}_{1}(α), but unprovable in T^{i}_{1}(α). This is in contrast with the classical situation, where S^{i+1}_{2} is conservative over T^{i}_{2} 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.
 Journal page PDF

Satisfiability problems complete for deterministic logarithmic space
Jan JohannsenIn: Volker Diekert and Michel Habib (eds.): STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. Springer LNCS 2996, pp. 317325, 2004.
The satisfiability and notallequal satisfiability problems for boolean formulas in CNF with at most two occurrences of each variable are complete for deterministic logarithmic space.
 Springer LNCS page, PDF

CTL^{+} is complete for double exponential time
Jan Johannsen and Martin LangeIn: J. C. M. Baeten et al., editors, Proc. 30th Int. Coll. on Automata, Logics and Programming (ICALP'03), Springer LNCS 2719, pp. 767775, 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 2EXPTIMEhard. The construction is inspired by Vardi and Stockmeyer's 2EXPTIMEhardness proof of CTL*'s satisfiability problem. As a consequence, there is no subexponential reduction from CTL^{+} to CTL which preserves satisfiability.
 Springer LNCS page, PDF

An Optimal Lower Bound for Resolution with 2Conjunctions
Jan Johannsen and N.S. NarayanaswamyProceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS) Springer LNCS 2420, pp. 387398
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.
An Exponential Separation between Regular and General Resolution
Michael Alekhnovich, Jan Johannsen, Toniann Pitassi and Alasdair Urquhart
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 0156, 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 quasipolynomial.
TOC page, ACM DL page (STOC version), ECCC
An Elementary Fragment of SecondOrder Lambda Calculus
Klaus Aehlig and Jan Johannsen
ACM Transactions on Computational Logic 6 no.2, pp. 468  480. Preliminary version available on CoRR as cs.LO/0210022
A fragment of secondorder lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be noninterleaved 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.
 Journal page, ArXiv page, PDF

Linear Ramified Higher Type Recursion and Parallel Complexity
Klaus Aehlig, Jan Johannsen, Helmut Schwichtenberg and Sebastiaan A. Terwijnin: R. Kahle, P. SchröderHeister, 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.
 Journal page PDF

Depth Lower Bounds for Monotone SemiUnbounded FanIn Circuits
Jan JohannsenRAIRO Theoretical Informatics and Applications 35(3) pp. 277286, 2001
The depth hierarchy results for monotone circuits of Raz and McKenzie (Combinatorica 19, 1999) are extended to the case of monotone circuits of semiunbounded fanin. It follows that the inclusions NC^{i} <= SAC^{i} <= AC^{i} are proper in the monotone setting, for every i>=1.
 Journal page PDF

Cumulative HigherOrder Logic as a Foundation for Set Theory
J. Wolfgang Degen and Jan JohannsenMathematical Logic Quarterly 46 (2000) pp. 147170
The systems K_α of transfinite cumulative types up to α are extended to systems K_α^∞ that include a natural infinitary inference rule, the socalled limit rule. For countable α a semantic completeness theorem for K_α^∞ is proved by the method of reduction trees, and it is shown that every model of K_α^∞ is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic firstorder set theories can be interpreted in K_α^∞, for suitable α.
 Journal page, PDF

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi and Jan JohannsenSIAM Journal on Computing, Vol. 30, No. 5 (2000), pp. 14621484
An exponential lower bound for the size of treelike Cutting Planes refutations of a certain family of CNF formulas with polynomial size resolution refutations is proved. This implies an exponential separation between the treelike versions and the daglike 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 treelike resolution and several refinements of resolution: negative resolution and regular resolution. Actually this last separation also provides a separation between treelike 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).
 Journal page, PDF

On the Δ^{b}_{1}BitComprehension Rule
Jan Johannsen and Chris PollettIn: S. Buss, P. Hájek, P. Pudlák (eds.) "Logic Colloquium '98", ASL Lecture Notes in Logic, 2000
The theory Δ^{b}_{1}CR of Bounded Arithmetic axiomatized by the Δ^{b}_{1}bitcomprehension rule is defined and shown to be strongly related to the complexity class TC^{0}. The Σ^{b}_{1}definable functions of Δ^{b}_{1}CR are those in uniform TC^{0}, and the Σ^{b}_{2}definable functions are computable by counterexample computations using TC^{0}functions. The latter is used to show that a collapse of stronger theories to Δ^{b}_{1}CR implies that NP is contained in nonuniform TC^{0}.
Weak Bounded Arithmetic, the DiffieHellman 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 DLogTimeuniform TC^{0}, is extended by a function symbol and axioms for integer division, which is not known to be in DLogTimeuniform TC^{0}. About this extended theory C^0_2[div], two main results are proved:
1. The Σ^{b}_{1}definable functions of C^0_2[div] are exactly Constable's class K, a function algebra whose precise complexitytheoretic nature is yet to be determined. This also yields the new upper bound K \subseteq uniform NC^{2}.
2. The Δ^{b}_{1}theorems of C^0_2[div] do not have Craiginterpolants of polynomial circuit size, unless the DiffieHellman key exchange protocol is insecure.
 IEEE page, PDF

A Remark on Independence Results for Sharply Bounded Arithmetic
Jan JohannsenMathematical Logic Quarterly 44(4) pp. 568570, 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 modeltheoretic method developed by the author in his thesis and (MLQ 44(2), 1998).
On Proofs about Threshold Circuits and Counting Hierarchies (Extended Abstract)
Jan Johannsen and Chris Pollett
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 constantdepth threshold circuits of polynomial and quasipolynomial size. Then we define certain secondorder 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 socalled RSUVisomorphism.
 IEEE page, PDF

Equational Calculi and ConstantDepth Propositional Proofs
Jan JohannsenIn: 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.
Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems
Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi and Jan Johannsen
Proceedings of the 39th IEEE Symposium on Foundations of Computer Science, Palo Alto, 1998
An exponential lower bound is proved for treelike Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between treelike and daglike 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 treelike resolution from (daglike) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a DavisPutnam resolution proof. This extends the corresponding superpolynomial separation of Urquhart (Bull. Symb. Logic 1, 1995).
Finally, an exponential separation is proved between DavisPutnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known from Goerdt (Ann. Math. Artificial Intelligence 6, 1992).
 IEEE page PDF

A ModelTheoretic Property of Sharply Bounded Formulae, with some Applications
Jan JohannsenMathematical Logic Quarterly 44(2) pp. 205215, 1998
We define a property of substructures of models of arithmetic, that of being lengthinitial, and show that sharply bounded formulae are absolute between a model and its lengthinitial submodels. We use this to prove independence results for some weak fragments of bounded arithmetic by constructing appropriate models as lengthinitial submodels of some given model.
 Journal page PDF

Lower Bounds for Monotone Real Circuit Depth and Formula Size and Treelike Cutting Planes
Jan JohannsenInformation Procesing Letters 67 (1) pp. 3741, 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 stconnectivity. This implies a superpolynomial speedup of daglike over treelike Cutting Planes proofs.
 Journal page PDF

A Bounded Aritmetic Theory for ConstantDepth Threshold Circuits
Jan JohannsenIn: P. Hájjek (ed.) "GÖDEL '96", Lecture Notes in Logic 6, pp. 224234, 1996
We define an extension \bar{R}^0_2 of the bounded arithmetic theory R^0_2 and show that the class of functions Σ^{b}_{1}definable in \bar{R}^0_2 coincides with the computational complexity class TC^{0} of functions computable by polynomial size, constantdepth threshold circuits.
 CUP Lecture Notes in Logic page, PDF

On Sharply Bounded Length Induction
Jan JohannsenIn: Proc. of Computer Science Logic '95, Paderborn 1995, Springer LNCS 1092, 1996
We construct models of the theory L_2^0 := BASIC + \Sigma^b_0LIND: one where the predecessor function is not total and one not satisfying \Sigma^b_0PIND, 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_0axiomatizable.
 Springer LNCS page, PDF

A Note on Sharply Bounded Arithmetic
Jan JohannsenArchive for Mathematical Logic 33 pp. 159165, 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_1formulae in extensions of R^0_2.
 Journal page, PDF

On the Weakness of Sharply Bounded Polynomial Induction
Jan JohannsenIn: G. Gottlob et al. (eds.) "Computational Logic and Proof Theory", Proceedings of KGC'93, Brno 1993, Springer LNCS 713, pp. 223230, 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_1define every function in AC^0, the class of functions computable by polynomial size constant depth circuits.
Artikelaktionen