Overview

The League of SAT Solvers is a fast-paced competition where participants test their solvers against challenging SAT instances. Matches occur hourly, last 45 minutes, and are open to solvers of all types—custom-built or pre-existing. The solvers are run on your local machine.

Participation

1. Solver Registration:

   • Anyone can join by registering a SAT solver on the league’s platform: After creation and log in into an account you can add a new solver.

   • Participants can compete using their own solvers or an existing solver from a public repository.

   • When using an existing solver, please give credit by linking the source code or mentioning the used solver in the description.

   • Names of existing solvers may be reassigned to the original solver author upon request.

2. Participating in a Match:

   • To participate download and follow the instructions of the official client: los-client

   • The client is open source, customization of the client is allowed.

3. No limitations on the solver:

   • By running on your own machine, there are no resource constraints on the solver. You can utilize all of your CPU, GPU, build an FPGA or set up a cluster to compete.

   • Currently, the server does not check UNSAT answers. It is OK to abuse this fact, but please be transparent about it in the solver description.

4. Fair Play:

   • Don’t try to crash or DOS the server. If you notice bugs or exploits please report them via the client issue tracker.

Match Format

1. Start Time:

   • Matches begin every full hour (e.g., 1:00 PM, 2:00 PM, etc.) and last for 45 minutes.

2. Registration Time:

   • Registration for matches starts roughly 15 minutes before the match.

3. Single-Instance Matches:

   • Each match involves solving one SAT instance, selected randomly from the league’s benchmark pool.

4. Winning Criteria:

   • The solver that provides the correct solution (SAT/UNSAT) the fastest wins. Incorrect answers result in immediate disqualification for that match. Disqualified solvers are ranked below solvers that do not finish within the time limit.

   • Instances are considered UNSAT unless at-least one solver provides a correct solution.

5. Tie-Breakers:

   • Ties are broken at random.

6. Benchmark Pool:

   • Benchmarks are currently mostly a selection of benchmarks from the SAT competition 2024 obtained via the Global Solver Database. However, the benchmark selection may change any time.

Technical Information about the Client Server Interaction

The client and match server communicate via a websocket. The communication works roughly as follows.

1. The client connects to the server and gets a welcome message.

2. The client sends the solver token for registration.

3. The server sends an encrypted instance to the client.

4. When the match starts the decryption key is sent to the client.

5. The client sends its answer (SAT/UNSAT) to the server. If the answer is SAT it also sends a hash of the solution.

6. The server records the time when it receives an answer.

7. While the match is still running, the client sends the full solution to the server.

8. When the match ends, the server stops accepting answers and checks the provided solutions. The server updates the solver rating based on the rank of the solver.