Sparkle SAT Challenge 2018

The Sparkle SAT Challenge 2018 is a novel competitive event that aims to assess the state of the art in solving the Boolean satisfiability (SAT) problem, leveraging cutting-edge automatically constructed algorithm selectors, and to quantify contributions of individual solvers.

It is well established that the state of the art for solving SAT is not defined by a single solver, but rather by a set of non-dominated solvers with complementary strengths. A prominent way of exploiting this performance complementarity is to leverage machine learning techniques to build effective automatic algorithm selectors on top of state-of-the-art SAT solvers. The Sparkle SAT Challenge automatically combines all participating solvers into a state-of-the-art algorithm selector for solving SAT, and assesses the contribution of each participating solver to the performance of that algorithm selector. It thus encourages submitters to make substantial contributions to the state of the art in SAT solving as realised by this selector, by maximising the contribution to overall selector performance due to their solver.

The Sparkle SAT Challenge 2018 is closely coordinated with the 2018 SAT Competition. In particular, working closely with the organisers of the 2018 SAT Competition, the Sparkle SAT Challenge 2018 will use the same test instances, the same cutoff time (5000 CPU sec) and the same base-line scoring scheme (PAR-2) as the Main Track of the 2018 SAT Competition. We strongly encourage all participants in the Sparkle SAT Challenge 2018 to also submit (variants) of their solvers to the Main Track of the 2018 SAT Competition and vice versa, keeping in mind that to do well in the Sparkle SAT Challenge, excellent stand-alone performance is not sufficient; instead, the best results will be achieved by solvers that make a large contribution to the performance of an algorithm selector build from all submitted solvers.

News

Mechanics

Solver developers will submit their solvers and supporting information via e-mail (see detailed information for Solver Submission below). During a period of 10 days before the submission deadline, every 24-48 hours, a state-of-the-art selector will be constructed, based on all solvers available at that time, using a set of training instances drawn from previous SAT competitions. The contributions to the performance of this selector, on the training set, will be published in a leader board accessible to all participants. During this phase, participants can resubmit their solvers as often as they desire.

Solver submissions need to list all authors, and no solver author can be involved in more than three separate submissions (not counting resubmissions, which replace previously submitted versions of a solver). Please note that submitting multiple solvers that perform well on very similar types of SAT instances can be expected to result in poor performance in the Sparkle challenge, since solvers are assessed based on their marginal contribution to overall selector performance.

The competition will be run on the Sparkle platform, a PbO-based problem-solving platform designed to enable the wide-spread and effective use of programming by optimisation (PbO) techniques for improving the state of the art in solving a broad range of prominent AI problems, including SAT and AI Planning. The Sparkle platform is being developed by the ADA Research Group, Leiden Institute of Advanced Computer Science (LIACS), Leiden University. The Sparkle challenge will be run on a large, state-of-the-art, Linux-based compute cluster at the Leiden Institute of Advanced Computer Science (LIACS).

The organisers of the Sparkle challenge will not participate in the challenge, nor in any track of the 2018 SAT Competition; organisers of the 2018 SAT Competition will not participate in the Sparkle challenge.

Prizes

Rather than the gold, silver and bronze medals awarded in traditional SAT competitions, participants in the Sparkle challenge will be awarded slices of a single gold medal; the size of each slice is proportional to the magnitude of the marginal contribution made by the respective solver to the performance of the automatically constructed selector built from all participating solvers on the same test set of instances used in the main track of the 2018 SAT Competition. Any solver that returns an incorrect solution to any training or test instance will be disqualified and removed from the set of solvers used in the final evaluation. Only open-source solvers are eligible for awards; closed-source solvers can participate, but will be running hors-concours in a separate, extended final evaluation that also includes all open-source solvers.

Important Dates

Solver Submission

The Sparkle SAT Challenge 2018 is coordinated with the 2018 SAT Competition and uses the same participation requirements as those for sequential solvers submitted to the SAT Competition (check here for details). Once your solver is prepared, please simply zip up your solver subdirectory and submit it (along with directions for building your solver from source) via e-mail to c.luo@liacs.leidenuniv.nl. (If the file is too large for an attachment, you can also e-mail us a link to it instead). After the competition, all submissions will be made publically available on this website; for this purpose, please provide a reference (e.g., bibtex entry) for your solver at submission time.

Apart from your solver archive, please also include the following information in your submission e-mail:

Organisers