6 citations · 12 across the 10 of their papers we have counts for
4 papers · 1 filter
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Leroy Chew, Alexis de Colnet, Friedrich Slivovsky +1
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraint…
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…
A Strongly Exponential Separation of DNNFs from CNF Formulas
Simone Bova, Florent Capelli, Stefan Mengel +1
Decomposable Negation Normal Forms (DNNFs) are Boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables.…
Model Counting for Formulas of Bounded Clique-Width
Friedrich Slivovsky, Stefan Szeider
We show that #SAT is polynomial-time tractable for classes of CNF formulas whose incidence graphs have bounded symmetric clique-width (or bounded clique-width, or bounded rank-widt…