Improving Combinatorial Bounds Using SAT Solvers

Title: Improving Combinatorial Bounds Using SAT Solvers

Abstract: This research explores the use of Satisfiability (SAT) solvers to improve combinatorial bounds, specifically focusing on van der Waerden numbers. The study demonstrates that recent advancements in SAT solvers have made it possible to obtain new results in combinatorics by encoding problems as propositional theories and then computing their models using general-purpose SAT solvers. The paper also argues that combinatorics is a rich source of structured, parameterized families of hard propositional theories, which can be used to benchmark and test new generations of SAT solvers.

Main Research Question: Can SAT solvers be used to improve combinatorial bounds, specifically for van der Waerden numbers?

Methodology: The study uses SAT solvers such as POSIT, SATO, and walkaspps, which are designed to compute models for propositional theories extended by cardinality atoms. These solvers are applied to the problem of computing van der Waerden numbers, which involve finding the least number of integers such that every partition of the numbers has an arithmetic progression of a specific length.

Results: The research shows that SAT solvers can improve lower bounds for van der Waerden numbers for several combinations of parameters. The study also reveals that the theories resulting from these combinatorial problems show a substantial degree of structure and similarity, suggesting that they could serve as benchmark theories for experiments with SAT solvers.

Implications: This research has several implications. First, it demonstrates that SAT solvers can be used to improve combinatorial bounds, providing a new approach to solving these problems. Second, it suggests that combinatorial problems can be used to benchmark and test new generations of SAT solvers, potentially leading to further advancements in the field. Lastly, the study highlights the potential of using SAT solvers in other areas of combinatorics and mathematics, opening up new avenues for research and exploration.

Link to Article: https://arxiv.org/abs/0310064v1 Authors: arXiv ID: 0310064v1