The SAT Competition 2021 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem organized as a satellite event to the 24th International Conference on Theory and Applications of Satisfiability Testing. It stands in the tradition of the yearly SAT Competitions and SAT-Races / Challenges. Solvers for the SAT problem have widespread applications in industry and research. Many problems (e.g., in hardware and software verification) that seemed out of range a decade ago can now be tackled routinely. The competition aims for new challenging benchmarks, promotion of SAT Solvers and their development, and evaluation of the current state-of-the-art solvers.
The Special Innovation Price was awarded to Benjamin Kaiser and Robert Clausecker for their submission of the SAT Solver CaDiCaL_PriPro to this years competition. CaDiCaL_PriPro is a SAT Solver based on conflict driven clause learning (CDCL) in which some clauses that were recently used for clause learning are severely prioritized during a process called propagation (PriPro). Utilizing this new idea CaDiCaL_PriPro was able to solve 21 of the 400 competition’s problems faster than any other solver. At the same time, CaDiCaL_PriPro is an overall good SAT Solver finishing 10th in the main track. Particularly, CaDiCaL_PriPro is strong on unsatisfiable instances where it finished 8th in a tight race decided by only a handful of problems. The election for the award is related to beingpart of the fastest 2-portfolio of all 48 participating solvers.
