5 papers
Orbitopal Fixing in SAT
Markus Anders, Cayden Codel, Marijn J. H. Heule
Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones alrea…
On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting
Ratip Emin Berker, Emanuel Tewolde, Vincent Conitzer +3
Core stability is a natural and well-studied notion for group fairness in multi-winner voting, where the task is to select a committee from a pool of candidates. We study the setti…
Unfolding Boxes with Local Constraints
Long Qian, Eric Wang, Bernardo Subercaseaux +1
We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, incl…
Automated Symmetric Constructions in Discrete Geometry
Bernardo Subercaseaux, Ethan Mackey, Long Qian +1
We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discoveri…
Certified Knowledge Compilation with Application to Formally Verified Model Counting
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad +1
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when form…