Verified SAT Competition

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

• When and where? Thursday, 6th December 2019 from 5pm-6.30pm at GHC 4.405.

Winners:

Misha Ivkov (best unit-sat)

Kevin Geng (best final-sat)

Lawrence Wang (best final-sat)

Katia Villevald (3rd place)

Philip Wang (best verified)

Jared Moore (random winner)

Detailed results can be found in the slides presented during this event. Below we have some photos taken from the event. We would like to thank everyone for participating in this event and for making the first verified SAT competition a big success!

Details

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

Prizes

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

• Free food for everyone!
• T-shirts for all students!
• Amazon vouchers for the authors of the best verified solvers and for a random winner!
• Glory and fame for winning the first verified SAT competition!

Ranking

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:

• Competition_time = CPU_time * (2.5-Verification_score)

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.5-0.8) = 170 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.

Benchmarks

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

• Combinatorial problems such as the pigeon hole problem:
• These instances were generated with CNFGen.
• Software model checking problems:
• These instances were generated with CBMC.