22 citations · 90 across the 29 of their papers we have counts for
19 papers · 1 filter
Bounds on BDD-Based Bucket Elimination
Stefan Mengel
We study BDD-based bucket elimination, an approach to satisfiability testing using variable elimination which has seen several practical implementations in the past. We prove that…
No Efficient Disjunction or Conjunction of Switch-Lists
Stefan Mengel
It is shown that disjunction of two switch-lists can blow up the representation size exponentially. Since switch-lists can be negated without any increase in size, this shows that…
Lower Bounds on Intermediate Results in Bottom-Up Knowledge Compilation
Alexis de Colnet, Stefan Mengel
Bottom-up knowledge compilation is a paradigm for generating representations of functions by iteratively conjoining constraints using a so-called apply function. When the input is…
A Compilation of Succinctness Results for Arithmetic Circuits
Alexis de Colnet, Stefan Mengel
Arithmetic circuits (AC) are circuits over the real numbers with 0/1-valued input variables whose gates compute the sum or the product of their inputs. Positive AC -- that is, AC r…
Proof Complexity of Symbolic QBF Reasoning
Stefan Mengel, Friedrich Slivovsky
We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers t…
Characterizing Tseitin-formulas with short regular resolution refutations
Alexis de Colnet, Stefan Mengel
Tseitin-formulas are systems of parity constraints whose structure is described by a graph. These formulas have been studied extensively in proof complexity as hard instances in ma…