Verified SAT Competition

This year, we will organize the first verified SAT competition where we will assess the performance of your verified SAT solvers!

SAT solvers can be used to check the correctness of real-world code. However, the SAT solver itself is also a piece of software and needs to be verified. During this course, you developed and verified a simple SAT solver with and without unit propagation. Using our reference implementation for simple-sat (Lab 3) and unit-sat (Lab 4), we can see the impact of unit propagation on the performance of the SAT solver.

Your browser does not support the HTML 5 canvas element


This competition is supported by a ProSEED/Crosswalk grant and we will have:


Solvers will be ranked according to the number of instances solved within 600 seconds. Since we encourage fully verified SAT solvers in this course, the time will be weighted with a verification score (value in [0,1]) as follows:

For example, if for a given instance your solver took 100 seconds to solve it but your solver is not fully verified and got a verification score of 0.8 then the competition time will be of 100*(2-0.8) = 120 seconds. If two solvers solve the same number of instances, we will use average time as the tie breaker.

If your solver is not fully verified and reports an incorrect answer (satisfiable for unsatisfiable instances or unsatisfiable for satisfiable instances) than your solver will be disqualified from the competition.

All solvers will be ran on StarExec with a 600 seconds time limit and 32 GB memory limit.


This verified SAT competition will take your verified SAT solver to the limit and see how well it performs when solving 100 problems from: