5 citations · 8 across the 14 of their papers we have counts for
18 papers
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…
A SAT Attack on Tarski's High School Algebra Problem
Bernardo Subercaseaux, Benjamin Przybocki
Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 element…
Toward Satisfiability Modulo Realizability
Andrew Krapivin, Benjamin Przybocki, Marijn J. H. Heule
Problems complete for the existential theory of the reals () arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based a…
Bringing closure to theory combination properties
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
We consider the closure of three classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness…
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
Benjamin Przybocki, John Mackey, Marijn J. H. Heule +1
Ramsey-good graphs are graphs that contain neither a clique of size nor an independent set of size . We study doubly saturated Ramsey-good graphs, defined as Ramsey-good gra…
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…
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…
Accelerating Scientific Research with Gemini: Case Studies and Common Techniques
David P. Woodruff, Vincent Cohen-Addad, Lalit Jain +33
Recent advances in large language models (LLMs) have opened new avenues for accelerating scientific research. While models are increasingly capable of assisting with routine tasks,…
Characterizing Sets of Theories That Can Be Disjointly Combined
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describ…
Optimal and Efficient Partite Decompositions of Hypergraphs
Andrew Krapivin, Benjamin Przybocki, Nicolás Sanhueza-Matamala +1
We study the problem of partitioning the edges of a -uniform hypergraph into a family of complete -partite hypergraphs (-cliques). We show that there is a partitio…
Shininess, strong politeness, and unicorns
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal an…
Being polite is not enough (and other limits of theory combination)
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and th…
The termination of Nielsen transformations applied to word equations with length constraints
Benjamin Przybocki, Clark Barrett
Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminat…
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
Benjamin Przybocki, Guilherme Toledo, Yoni Zohar +1
Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are…
Bender-Knuth involutions on linear extensions of posets
Judy Hsin-Hui Chiang, Anh Trong Nam Hoang, Matthew Kendall +4
We study the permutation group generated by Bender-Knuth moves on linear extensions of a poset , an analog of the Berenstein-Kirillov group on column-strict tab…
The maximum hook length of -distinct simultaneous core partitions
Ethan Pesikoff, Benjamin Przybocki, Janabel Xia
We exactly determine the maximum possible hook length of -core partitions with -distinct parts when there are finitely many such partitions. Moreover, we provide an algor…
Lengths of Irreducible and Delicate Words
Benjamin Przybocki
We study words that barely avoid repetitions, for several senses of "barely". A squarefree (respectively, overlap-free, cubefree) word is irreducible if removing any one of its int…
Hat Guessing on Books and Windmills
Xiaoyu He, Yuzu Ido, Benjamin Przybocki
The hat-guessing number is a graph invariant defined by Butler, Hajiaghayi, Kleinberg, and Leighton. We determine the hat-guessing number exactly for book graphs with sufficiently…