SAT Gory details

During his invited talk at the SAT conference, Moshe Vardi made the point that the SAT competition might harm the SAT community in the long term because the part of the community interested in practical aspects of SAT solving roughly reached monoculture.

It is true that since the first SAT competition in 2002, the diversity of SAT solvers is reduced: 4 CDCL solvers only in 2002 while nowadays around 2/3 of the solvers, and basically all the ones tailored for application benchmarks, are CDCL ones.

Moshes Vardi claims that researchers are currently focusing on an approach known to work well currently but might miss to build the approach that will work well in the future. His main point was that CDCL solvers are still based on the resolution proof system while more powerful proof systems exists (e.g. extended resolution, cutting planes, etc).
Replacing resolution inference by cutting planes has already been investigated by various researchers (Chai and Kuellmann in Galena, Heidi Dixon in PBChaff, Sheini and Sakalah in Pueblo, etc) but the results are currently not convincing: see e.g. SAT4J at the Pseudo Boolean evaluation: the resolution proof system based one (SAT4J Pseudo Resolution) performs globally better than the cutting planes proof system based one (SAT4J Pseudo Cutting Planes).

In my opinion, there are pretty positive consequences of the SAT competition that make the SAT competition a good thing for the SAT community:

• The competition is supported by the community: with about 50 SAT solvers from about 30 teams from all over the world each time, it is a widely adopted event in the SAT community.
• The competition emphasize state-of-the-art solvers regularly: it is easy for anybody willing to evaluate SAT technology to grab a recent efficient solver an give it a try.
• The competition spreads coding tricks and algorithmic improvements among solvers designers: by forcing competitors to release the source code of their solvers for research purposes, technical details that are not found in scientific papers are available to anybody willing to dive into those details.
• Maybe even more important: the SAT competition allowed the availability of many robust, efficient, easy to embed SAT solvers that allowed people outside the SAT community to find new use of SAT technology. SAT solvers moved from proof of concept software to highly reliable and carefully designed software.

Regarding monoculture, the competition has several categories that allow various kind of SAT solvers to be awarded. The competition also tried to point out singular solvers (Allen van Gelder’s purse score). We are open to any suggestions that could favor the emergence of new generations of SAT solvers.