SAT4Math

92 papers


  • Investigating Simple Drawings of K_n Using SAT
    Bergold, Scheucher
    arXiv '25
    graph drawing
  • Counterexample to Winkler's Conjecture on Venn Diagrams
    Brenner, Kleist, Mütze, Rieck, Verciani
    arXiv '25
    counterexamples
  • Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems
    Li, Duggan, Bright, Ganesh
    arXiv '25
    IJCAI '25
    computer algebra
    Ramsey theory
  • Smart Cubing for Graph Search: A Comparative Study
    Kirchweger, Xia, Peitl, Szeider
    arXiv '25
    graph theory
  • Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
    Van Caudenberg, Bogaerts, Vendramin
    arXiv '25
    TACAS '25
    algebra
  • The Borsuk Problem for Subsets of the Vertices of the 10-Dimensional Boolean Cube
    Batmanov, Voronov
    arXiv '25
  • Myrvold's Results on Orthogonal Triples of 10 x 10 Latin Squares: A SAT Investigation
    Bright, Keita, Stevens
    arXiv '25
    combinatorial design
  • Algebraic and SAT Models for SCA Generation
    Koelbing, Garn, Iurlano, Kotsireas, Simos
    Appl. Algebra Eng. Commun. Comput. '25
    sequence covering arrays
  • Optimal Partitions of the Flat Torus into Parts of Smaller Diameter
    Protasov, Tolmachev, Voronov
    Discrete Optimization '25
  • Lower Bounds for Book Ramsey Numbers
    Wesley
    arXiv '24
    Ramsey theory
  • Proving Norine's Conjecture Holds for $n = 7$ via SAT Solvers
    Frankston, Scheinerman
    arXiv '24
    graph coloring
  • SAT and Lattice Reduction for Integer Factorization
    Ajani, Bright
    arXiv '24
    ISSAC '24
    integer factorization
  • Using Finite Automata to Compute the Base-b Representation of the Golden Ratio and Other Quadratic Irrationals
    Barnoff, Bright, Shallit
    arXiv '24
    CIAA '24
    automata theory
    irrational numbers
  • A Formal Proof of R(4,5)
    Gauthier, Brown
    arXiv '24
    Ramsey theory
  • Happy Ending: An Empty Hexagon in Every Set of 30 Points
    Heule, Scheucher
    arXiv '24
    TACAS '24
    discrete geometry
    Ramsey theory
  • Finding Hardness Reductions Automatically Using SAT Solvers
    Bergold, Scheucher, Schröder
    arXiv '24
    gadget design
  • A SAT Solver + Computer Algebra Attack on the Minimum Kochen-Specker Problem
    Li, Bright, Ganesh
    IJCAI '24
    vector systems
  • SAT-Based Search for Minwise Independent Families
    Iurlano, Raidl
    arXiv '24
  • PackIt! Gamified Rectangle Packing
    Garrison, Heule, Subercaseaux
    arXiv '24
    FUN '24
    combinatorial games
  • Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries
    Kirchweger, Szeider
    CP '24
    graph theory
    social choice theory
  • SAT Modulo Symmetries for Graph Generation and Enumeration
    Kirchweger, Szeider
    ACM Trans. Comput. Log. '24
    graph theory
  • Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
    Subercaseaux, Mackey, Heule, Martins
    arXiv '23
    CICM '24
    discrete geometry
    Ramsey theory
  • Structure and Computability of Preimages in the Game of Life
    Salo, Törmä
    arXiv '23
    Theoretical Computer Science '25
    cellular automata
    gadget design
    recreational mathematics
  • On the Deque and Rique Numbers of Complete and Complete Bipartite Graphs
    Bekos, Kaufmann, Pavlidi, Rieger
    arXiv '23
    CCCG '23
    graph drawing
    graph theory
  • Co-Certificate Learning with SAT modulo Symmetries
    Kirchweger, Peitl, Szeider
    arXiv '23
    IJCAI '23
    vector systems
  • Using SAT to Study Plane Hamiltonian Substructures in Simple Drawings
    Bergold, Felsner, Reddy, Scheucher
    arXiv '23
    graph drawing
  • An Extension Theorem for Signotopes
    Bergold, Felsner, Scheucher
    arXiv '23
    SoCG '23
  • The Packing Chromatic Number of the Infinite Square Grid is 15
    Subercaseaux, Heule
    arXiv '23
    TACAS '23
    graph coloring
  • A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture
    Kirchweger, Peitl, Szeider
    SAT '23
    famous conjectures
    graph coloring
  • A SAT Attack on Erdős-Szekeres Numbers in R^d and the Empty Hexagon Theorem
    Scheucher
    Comput. Geom. Topol. '23
    discrete geometry
    Ramsey theory
  • On a Pair of Orthogonal Golf Designs
    Lu, Chen, Cao
    Discrete Mathematics '23
  • Investigating the~Existence of~Holey Latin Squares via~Satisfiability Testing
    Liu, Han, Jia, Huang, Ma, Zhang, Zhang
    PRICAI '23
    combinatorial design
  • Toward Optimal Radio Colorings of Hypercubes via SAT-solving
    Subercaseaux, Heule
    LPAR '23
    graph coloring
  • Using a SAT Solver to Find Interesting Sets of Nonstandard Dice
    Purcell
    Am. Math. Mon. '23
    recreational mathematics
  • Searching for Smallest Universal Graphs and Tournaments with SAT
    Zhang, Szeider
    CP '23
    graph theory
  • Rado Numbers and SAT Computations
    Chang, Loera, Wesley
    arXiv '22
    ISSAC '22
    Ramsey theory
  • New Lower Bounds for Cap Sets
    Tyrrell
    arXiv '22
    Ramsey theory
  • Impossibility Theorems Involving Weakenings of Expansion Consistency and Resoluteness in Voting
    Holliday, Norman, Pacuit, Zahedian
    arXiv '22
    social choice theory
  • Improved Lower Bounds for Multicolour Ramsey Numbers using SAT-Solvers
    Rowley
    arXiv '22
    Ramsey theory
  • New lower bounds for Schur and weak Schur numbers
    Ageron, Casteras, Pellerin, Portella, Rimmel, Tomasik
    arXiv '21
    Ramsey theory
  • On Using SAT Solvers for Graph Computations
    Courcelle, Durand
    preprint '22
    graph theory
  • The Packing Chromatic Number of the Infinite Square Grid Is at Least 14
    Subercaseaux, Heule
    SAT '22
    graph coloring
  • When Satisfiability Solving Meets Symbolic Computation
    Bright, Kotsireas, Ganesh
    Commun. ACM '22
    survey
  • A SAT Attack on Rota's Basis Conjecture
    Kirchweger, Scheucher, Szeider
    SAT '22
    famous conjectures
    matroids
  • An Automated Approach to the Collatz Conjecture
    Yolcu, Aaronson, Heule
    arXiv '21
    J. Autom. Reason. '23
    famous conjectures
  • A Counterexample to the Unit Conjecture for Group Rings
    Gardam
    Annals of Mathematics '21
    arXiv '21
    algebra
    famous conjectures
  • Avoiding Monochromatic Rectangles Using Shift Patterns
    Liu, Chew, Heule
    arXiv '20
    SOCS '21
    Ramsey theory
  • A SAT-based Resolution of Lam's Problem
    Bright, Cheung, Stevens, Kotsireas, Ganesh
    AAAI '21
    arXiv '20
    combinatorial design
  • Farad\v zev Read-type Enumeration of Non-Isomorphic CC Systems
    Bankovi{\'c}, Mari{\'c}
    Computational Geometry '21
  • Tighter Bounds on Directed Ramsey Number R(7)
    Neiman, Mackey, Heule
    arXiv '20
    Graphs Comb. '22
    Ramsey theory
  • Coloring Unit-Distance Strips Using SAT
    Oostema, Martins, Heule
    LPAR '20
    graph coloring
  • A nonexistence certificate for projective planes of order ten with weight 15 codewords
    Bright, Cheung, Stevens, Roy, Kotsireas, Ganesh
    AAECC '20
    combinatorial design
  • The Resolution of Keller's Conjecture
    Brakensiek, Heule, Mackey, Narváez
    arXiv '19
    J. Autom. Reason. '22
    famous conjectures
  • Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
    Bright, Kotsireas, Heinle, Ganesh
    arXiv '19
    J. Symb. Comput. '21
    computer algebra
  • Effective Problem Solving Using SAT Solvers
    Bright, Gerhard, Kotsireas, Ganesh
    arXiv '19
    MC '19
    computer algebra
    survey
  • The SAT+CAS method for combinatorial search with applications to best matrices
    Bright, Dokovic, Kotsireas, Ganesh
    Ann. Math. Artif. Intell. '19
    computer algebra
    linear algebra
  • SAT solvers and computer algebra systems: a powerful combination for mathematics
    Bright, Kotsireas, Ganesh
    CASCON '19
    computer algebra
  • Fast Formal Proof of the Erd\H os--Szekeres Conjecture for Convex Polygons with at Most 6 Points
    Mari{\'c}
    Journal of Automated Reasoning '19
  • On Orthogonal Symmetric Chain Decompositions
    Däubel, Jäger, Mütze, Scheucher
    arXiv '18
    Electron. J. Comb. '19
    poset theory
  • On L-shaped Point Set Embeddings of Trees: First Non-Embeddable Examples
    Mütze, Scheucher
    arXiv '18
    J. Graph Algorithms Appl. '20
    discrete geometry
    graph drawing
  • Two Disjoint 5-Holes in Point Sets
    Scheucher
    arXiv '18
    Comput. Geom. '20
    discrete geometry
  • Computing Small Unit-Distance Graphs with Chromatic Number 5
    Heule
    arXiv '18
    graph coloring
  • The Chromatic Number of the Plane Is at Least 5
    de Grey
    arXiv '18
    graph coloring
  • Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
    Bright, Kotsireas, Ganesh
    arXiv '18
    J. Symb. Comput. '20
    linear algebra
  • Improving Circuit Size Upper Bounds Using SAT-solvers
    Kulikov
    DATE '18
    circuit complexity
  • Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
    Huang, Ma, Ge, Zhang, Zhang
    Automated {{Reasoning}} '18
  • A SAT+CAS Method for Enumerating Williamson Matrices of Even Order
    Bright, Kotsireas, Ganesh
    AAAI '18
    linear algebra
  • Schur Number Five
    Heule
    AAAI '18
    arXiv '17
    Ramsey theory
  • A SAT Attack on the Erdős-Szekeres Conjecture
    Balko, Valtr
    Eur. J. Comb. '17
    discrete geometry
    Ramsey theory
  • Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
    Zulkoski, Bright, Heinle, Kotsireas, Czarnecki, Ganesh
    J. Autom. Reason. '17
    computer algebra
    graph theory
  • The Science of Brute Force
    Heule, Kullmann
    Commun. ACM '17
    survey
  • Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
    Heule, Kullmann, Marek
    arXiv '16
    SAT '16
    famous conjectures
    Ramsey theory
  • MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
    Bright, Ganesh, Heinle, Kotsireas, Nejati, Czarnecki
    CASC '16
    computer algebra
  • Non Existence of Some Mixed Moore Graphs of Diameter 2 Using SAT
    López, Miret, Fernández
    Discret. Math. '16
    graph theory
  • Computing the Ramsey Number R(4,3,3) Using Abstraction and Symmetry Breaking
    Codish, Frank, Itzhakov, Miller
    arXiv '15
    Constraints An Int. J. '16
    Ramsey theory
  • Optimal-Depth Sorting Networks
    Bundala, Codish, Cruz-Filipe, Schneider-Kamp, Závodný
    arXiv '14
    J. Comput. Syst. Sci. '17
    sorting networks
  • The Book Embedding Problem from a SAT-Solving Perspective
    Bekos, Kaufmann, Zielke
    GD '15
    graph drawing
  • MathCheck: A Math Assistant via a Combination of Computer Algebra
    Zulkoski, Ganesh, Czarnecki
    CADE '15
    computer algebra
  • A SAT Attack on the Erdős Discrepancy Conjecture
    Konev, Lisitsa
    arXiv '14
    SAT '14
    famous conjectures
  • Symmetry in Gardens of Eden
    Hartman, Heule, Kwekkeboom, Noels
    Electron. J. Comb. '13
    cellular automata
    recreational mathematics
  • Breaking Symmetries in Graph Representation
    Codish, Miller, Prosser, Stuckey
    IJCAI '13
    graph theory
  • Upward Planarity Testing via SAT
    Chimani, Zeranski
    GD '12
    graph theory
  • Solving Rubik's Cube Using SAT Solvers
    Chen
    arXiv '11
    combinatorial games
  • Generating and Searching Families of FFT Algorithms
    Haynal, Haynal
    arXiv '11
  • Green-Tao Numbers and SAT
    Kullmann
    arXiv '10
    SAT '10
    Ramsey theory
  • A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
    Soh, Inoue, Tamura, Banbara, Nabeshima
    Fundamenta Informaticae '10
  • Finding Reductions Automatically
    Crouch, Immerman, Moss
    Fields of Logic and Computation '10
    gadget design
  • Two New Van Der Waerden Numbers: W(2; 3, 17) and w(2; 3, 18)
    Ahmed
    INTEGERS '10
    Ramsey theory
  • Combinatorial Designs by SAT Solvers
    Zhang
    Handbook of Satisfiability '09
    combinatorial design
    survey
  • The van Der Waerden Number W(2,6) Is 1132
    Kouril, Paul
    Exp. Math. '08
    Ramsey theory
  • Applying SAT Solving in Classification of Finite Algebras
    Meier, Sorge
    J. Autom. Reason. '05
    SAT '05
    algebra
  • Satisfiability and Computing van Der Waerden Numbers
    Dransfield, Marek, Truszczyński
    arXiv '03
    SAT '04
    Ramsey theory

algebra
automata theory
cellular automata
circuit complexity
combinatorial design
combinatorial games
computer algebra
counterexamples
discrete geometry
famous conjectures
gadget design
graph coloring
graph drawing
graph theory
integer factorization
irrational numbers
linear algebra
matroids
poset theory
Ramsey theory
recreational mathematics
sequence covering arrays
social choice theory
sorting networks
survey
vector systems