5 citations · 8 across the 14 of their papers we have counts for
Showing cs.CCShow all
2 papers · 1 filter
cs.CC2026
Automated Reencoding Meets Graph Theory
Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule
Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can…
cs.CC2026
Near-Optimal Encodings of Cardinality Constraints
Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux
We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques…