22 citations · 90 across the 29 of their papers we have counts for
4 papers · 2 filters
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…