7 papers
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…
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,…
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…