A novel SAT solver for the Van der Waerden numbers

Abstract

Abstract This paper introduces a new efficient satisfiability problem (SAT) solver, negative-literal Van der Waerden numbers SAT solver (NegVanSAT). It is a modification of the well-known SAT solver MINISAT where the constructor of the literals has been adjusted to start with the negated literals first. It reduces the calculations needed to solve a problem. The NegVanSAT is specifically designed for solving the satisfiability problem of finding Van der Waerden numbers, which are known to be very difficult to compute. Comparisons between the MINISAT and the proposed NegVanSAT show that the latter outperforms the MINISAT in finding many of them.

Keywords

• Satisfiability
• Van der Waerden numbers
• DPLL
• SAT solvers
• MINISAT