Arrow Research search

Author name cluster

Jan Johannsen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers
2 author rows

Possible papers

10

SAT Conference 2020 Conference Paper

Simplified and Improved Separations Between Regular and General Resolution by Lifting

  • Marc Vinyals
  • Jan Elffers
  • Jan Johannsen
  • Jakob Nordström

Abstract We give a significantly simplified proof of the exponential separation between regular and general resolution of Alekhnovich et al. (2007) as a consequence of 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.

Details

SAT Conference 2016 Conference Paper

Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers

  • Jan Elffers
  • Jan Johannsen
  • Massimo Lauria
  • Thomas Magnard
  • Jakob Nordström
  • Marc Vinyals

Abstract 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.

Details

SAT Conference 2013 Conference Paper

Exponential Separations in a Hierarchy of Clause Learning Proof Systems

  • Jan Johannsen

Abstract Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments \(\ensuremath{\ensuremath{\mathrm{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 \(\ensuremath{\ensuremath{\mathrm{RTL}} ({k})}\) and \(\ensuremath{\ensuremath{\mathrm{RTL}} ({k+1})}\) is shown.

Details

IJCAI Conference 2011 Conference Paper

Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width

  • Eli Ben-Sasson
  • Jan Johannsen

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.

PDF Details DOI

SAT Conference 2010 Conference Paper

Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas

  • Eli Ben-Sasson
  • Jan Johannsen

Abstract 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.

Details

SAT Conference 2009 Conference Paper

An Exponential Lower Bound for Width-Restricted Clause Learning

  • Jan Johannsen

Abstract It has been observed empirically that clause learning does not significantly improve the performance of a satisfiability 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.

Details

MFCS Conference 2002 Conference Paper

An Optimal Lower Bound for Resolution with 2-Conjunctions

  • Jan Johannsen
  • N. S. Narayanaswamy

Abstract 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.

Details

FOCS Conference 1998 Conference Paper

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

  • Maria Luisa Bonet
  • Juan Luis Esteban
  • Nicola Galesi
  • Jan Johannsen

We prove an exponential lower bound 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, we extend the lower bounds on the depth of monotone circuits of R. Raz and P. McKenzie (1997) to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution front (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Puatam resolution proof. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separations was previously known.

Details

CSL Conference 1996 Conference Paper

On Sharply Bounded Length Induction

  • Jan Johannsen

Abstract We construct models of the theory L 0 2: = BASIC + Σ b 0 - LIND: one where the predecessor function is not total and one not satisfying Σ 2 0 - PIND, showing that L 0 2 is strictly weaker that S 0 2. The construction also shows that S 0 2 is not ∀ ∑ b 0 -axiomatizable.

Details
v2026.09.13