1 citations · 1 across the 5 of their papers we have counts for
4 papers · 1 filter
Compilation and Fast Model Counting beyond CNF
Alexis de Colnet, Stefan Szeider, Tianwei Zhang
Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our the…
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…
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…
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…