6 citations · 16 across the 14 of their papers we have counts for
6 papers · 1 filter
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism
Christoph Berkholz, Moritz Lichter, Harry Vinall-Smeeth
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz (TOCL 2023) showed that there is a resolution refutation of narrow widt…
Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
Christoph Berkholz, Jakob Nordström
We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of -element structures that can be distinguished by a $…
On the speed of constraint propagation and the time complexity of arc consistency testing
Christoph Berkholz, Oleg Verbitsky
Establishing arc consistency on two relational structures is one of the most popular heuristics for the constraint satisfaction problem. We aim at determining the time complexity o…
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy
Christoph Berkholz, Andreas Krebs, Oleg Verbitsky
Given two structures and distinguishable in $\fo k$ (first-order logic with variables), let denote the minimum alternation depth of a $\fo k$ formula disting…
Lower Bounds for Existential Pebble Games and k-Consistency Tests
Christoph Berkholz
The existential k-pebble game characterizes the expressive power of the existential-positive k-variable fragment of first-order logic on finite structures. The winner of the existe…
On the Complexity of Finding Narrow Proofs
Christoph Berkholz
We study the complexity of the following "resolution width problem": Does a given 3-CNF have a resolution refutation of width k? We prove that the problem cannot be decided in time…