SAT for Mathematics
Papers and resources on using satisfiability solvers in mathematics.
Browse the papers
2003
2026
Newest first
126 papers
A SAT Attack on Tarski's High School Algebra Problem
Voting Method Synthesis on an Infinite Domain: A Possibility Theorem for Positive Involvement
One-Weight Colorings, the Symmetric Class, and Lower Bounds for Hales--Jewett Numbers
A Lean-Certified Proof of
There are matroid toric ideals without quadratic Gröbner bases
Witness-split + window-cardinality refinement for : Architecture, empirical results, and a structural hard pocket
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
A Counterexample to EFX Agents, Items, Submodular Valuations via SAT-Solving
A SAT-based Filtering Framework for Exact Coverings of K33 by Cliques of Order 3, 4 or 5
Constraint Satisfaction Programming for the No-three-in-line Problem
Two-colorings of finite grids: variations on a theorem of Tibor Gallai
North-East Lattice Paths Avoiding Collinear Points via Satisfiability
OOPS: Optimized One-Planarity Solver via SAT
From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin's Conjecture via SAT
Depth-13 Sorting Networks for 28 Channels
A note on irreducibility for topical maps
New bounds for some small multicolor Ramsey numbers
Queen Domination by SAT Solving
The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators
Constructing Optimal Kobon Triangle Arrangements via Table Encoding, SAT Solving, and Heuristic Straightening
Constructing strong starters of orders : triplication with SAT solver
Unfolding Boxes with Local Constraints
Automated Symmetric Constructions in Discrete Geometry
Investigating Simple Drawings of K_n Using SAT
Counterexample to Winkler's Conjecture on Venn Diagrams
Regional Controllability of Cellular Automata as a SAT Problem
Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems
Smart Cubing for Graph Search: A Comparative Study
Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
Algebraic and SAT Models for SCA Generation
Myrvold's Results on Orthogonal Triples of 10 x 10 Latin Squares: A SAT Investigation
Optimal Partitions of the Flat Torus into Parts of Smaller Diameter
The Borsuk Problem for Subsets of the Vertices of the 10-Dimensional Boolean Cube
Lower Bounds for Book Ramsey Numbers
Proving Norine's Conjecture Holds for via SAT Solvers
The chromatic number of 4-dimensional lattices
SAT and Lattice Reduction for Integer Factorization
Detecting Isohedral Polyforms with a SAT Solver
Using Finite Automata to Compute the Base-b Representation of the Golden Ratio and Other Quadratic Irrationals
A Formal Proof of R(4,5)=25
Happy Ending: An Empty Hexagon in Every Set of 30 Points
Finding Hardness Reductions Automatically Using SAT Solvers
A SAT Solver + Computer Algebra Attack on the Minimum Kochen-Specker Problem
Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries
PackIt! Gamified Rectangle Packing
SAT Modulo Symmetries for Graph Generation and Enumeration
SAT-Based Search for Minwise Independent Families
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
Structure and Computability of Preimages in the Game of Life
The Pancake Graph of Order 10 Is 4-Colorable
On the Deque and Rique Numbers of Complete and Complete Bipartite Graphs
Co-Certificate Learning with SAT modulo Symmetries
Using SAT to Study Plane Hamiltonian Substructures in Simple Drawings
An Extension Theorem for Signotopes
Computer-Aided Constructions of Commafree Codes
The Packing Chromatic Number of the Infinite Square Grid is 15
A SAT Attack on Erdős-Szekeres Numbers in R^d and the Empty Hexagon Theorem
A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture
Combinatorial Designs Meet Hypercliques: Higher Lower Bounds for Klee’s Measure Problem and Related Problems in Dimensions d ≥ 4
Investigating the~Existence of~Holey Latin Squares via~Satisfiability Testing
On a Pair of Orthogonal Golf Designs
Searching for Smallest Universal Graphs and Tournaments with SAT
Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Using a SAT Solver to Find Interesting Sets of Nonstandard Dice
Rado Numbers and SAT Computations
New Lower Bounds for Cap Sets
Impossibility Theorems Involving Weakenings of Expansion Consistency and Resoluteness in Voting
Improved Lower Bounds for Multicolour Ramsey Numbers using SAT-Solvers
A SAT Attack on Rota's Basis Conjecture
On Using SAT Solvers for Graph Computations
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14
When Satisfiability Solving Meets Symbolic Computation
New lower bounds for Schur and weak Schur numbers
An Automated Approach to the Collatz Conjecture
A Counterexample to the Unit Conjecture for Group Rings
Faradžev Read-type Enumeration of Non-Isomorphic CC Systems
Avoiding Monochromatic Rectangles Using Shift Patterns
A SAT-based Resolution of Lam's Problem
Tighter Bounds on Directed Ramsey Number R(7)
Zero-sum squares in -matrices with low discrepancy
Search for developments of a box having multiple ways of folding by SAT solver
A nonexistence certificate for projective planes of order ten with weight 15 codewords
Coloring Unit-Distance Strips Using SAT
The Resolution of Keller's Conjecture
Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
Effective Problem Solving Using SAT Solvers
Fast Formal Proof of the Erdős--Szekeres Conjecture for Convex Polygons with at Most 6 Points
SAT solvers and computer algebra systems: a powerful combination for mathematics
The SAT+CAS method for combinatorial search with applications to best matrices
On Orthogonal Symmetric Chain Decompositions
On L-shaped Point Set Embeddings of Trees: First Non-Embeddable Examples
Two Disjoint 5-Holes in Point Sets
Computing Small Unit-Distance Graphs with Chromatic Number 5
The Chromatic Number of the Plane Is at Least 5
Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
A SAT+CAS Method for Enumerating Williamson Matrices of Even Order
Improving Circuit Size Upper Bounds Using SAT-solvers
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Schur Number Five
A SAT Attack on the Erdős-Szekeres Conjecture
Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
The Science of Brute Force
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
Non Existence of Some Mixed Moore Graphs of Diameter 2 Using SAT
Computing the Ramsey Number R(4,3,3) Using Abstraction and Symmetry Breaking
MathCheck: A Math Assistant via a Combination of Computer Algebra
The Book Embedding Problem from a SAT-Solving Perspective
Optimal-Depth Sorting Networks
A SAT Attack on the Erdős Discrepancy Conjecture
Breaking Symmetries in Graph Representation
Solution of the Last Open Four-Colored Rectangle-Free Grid: An Extremely Complex Multiple-Valued Problem
Symmetry in Gardens of Eden
A New Lower Bound for the Ramsey Number R(4, 8)
Upward Planarity Testing via SAT
Solving Rubik's Cube Using SAT Solvers
Generating and Searching Families of FFT Algorithms
Green-Tao Numbers and SAT
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
Finding Reductions Automatically
Two New Van Der Waerden Numbers: W(2; 3, 17) and w(2; 3, 18)
Combinatorial Designs by SAT Solvers
The van Der Waerden Number W(2,6) Is 1132
Applying SAT Solving in Classification of Finite Algebras
Satisfiability and Computing van Der Waerden Numbers