Combining SAT Solvers with CAS to Verify Combinatorial Conjectures (2016)

This paper from 2016 presents a method that combines SAT solvers (computer programs that determine if a logical formula can be satisfied) with Computer Algebra Systems (CAS, such as Mathematica or Maple) to automatically verify combinatorial conjectures — mathematical statements about finite structures like graphs or sets. The key insight: SAT solvers are good at finding counterexamples quickly, while CAS excels at algebraic reasoning; by having them work together, the system can prove or disprove conjectures that neither tool could handle alone. The work is significant because many open problems in combinatorics (the branch of math dealing with counting, arrangements, and patterns) involve finite but large search spaces that are too big for brute-force checking, and this hybrid approach automates part of the verification process that previously required human insight.