Solvers

Every problem runs on every solver we have for its format, at the same time, on one machine with 8 vCPU and 16 GiB of memory. Each racer has 60 seconds. All of them are open source under permissive licenses.

How a winner is picked

• Optimization (LP, MPS, MaxSAT, MiniZinc, TSPLIB): the best checked objective among the racers that finished. A tie goes to the faster racer. When one racer proves optimality, the others are stopped.
• Yes-or-no problems (CNF, SMT-LIB, FlatZinc satisfaction): the first racer to answer sat or unsat.
• Factoring: the first racer to return factors.

How results are checked

We check every solution ourselves before we show it. The solver's own claim is not enough.

Format	Check
LP, MPS	Every row, bound and integrality restriction; objective recomputed
CNF	Every clause evaluated
WCNF	Hard clauses hold; soft cost recomputed
SMT-LIB	Model re-checked by the other solver
MiniZinc, FlatZinc	Variables fixed, model re-run as a checker
CP-SAT proto	OR-Tools validation of the assignment
TSPLIB	Tour is a permutation; length recomputed
Factor	Factors multiplied

Some claims cannot be checked cheaply: that a solution is optimal, a MIP's dual bound, and an UNSAT answer. Those are reported as the solver gave them and marked as solver-reported on the card.

Enter your own solver

Today the house supplies every racer. We want to open the race: your solver would run on problems whose owners ticked "public", the board would show when it wins, and over time the ranking would show which solver is best at what. We have not built that yet, and we will build it when there are solvers waiting and problems that our racers handle badly.

If you want in, leave your address and a line about your solver. We will write when it opens.