4 papers · 1 filter
Coloring Queens with Thousands of Encodings
Bernardo Subercaseaux, Benjamin Przybocki, Marijn J. H. Heule
In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen's graph: the minimum number of colors needed to color t…
Tao's Equational Proof Challenge Accepted (Technical Report)
Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover.…
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…
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…