Der SAT-Wettbewerb 2021 ist eine Wettbewerbsveranstaltung für Löser des Booleschen Erfüllbarkeitsproblems (SAT), die als Satellitenveranstaltung zur 24th International Conference on Theory and Applications of Satisfiability Testing stattfand. Sie steht in der Tradition der jährlich stattfindenden SAT-Wettbewerbe und SAT-Races / Challenges. Löser für das SAT-Problem haben weit verbreitete Anwendungen in Industrie und Forschung. Viele Probleme (z.B. in der Hardware- und Software-Verifikation), die vor einem Jahrzehnt noch unerreichbar schienen, können jetzt routinemäßig gelöst werden. Der Wettbewerb zielt auf neue anspruchsvolle Benchmarks, die Förderung von SAT-Solvern und deren Entwicklung, und Evaluierung der aktuellen State-of-the-Art Solver.
Der Sonderinnovationspreis wurde an Benjamin Kaiser und Robert Clausecker für ihre Einreichung des SAT Solvers CaDiCaL_PriPro zum diesjährigen Wettbewerb verliehen. CaDiCaL_PriPro nutzt konfliktgeleitetes Klausellernen (CDCL) bei dem kürzlich zum Klausellernen verwendete Klauseln während der weiteren Propagation stark priorisiert werden (PriPro). Mit dieser neuen Idee konnte CaDiCaL_PriPro 21 der 400 Wettbewerbsprobleme schneller lösen als jeder andere Solver. Insgesamt belegte CaDiCaL_PriPro den 10. Platz in der Hauptkategorie. Besonders stark ist CaDiCaL_PriPro bei unerfüllbaren Instanzen, wo er in einem knappen Rennen, das durch nur wenige Probleme entschieden wurde, den 8. Platz erreichte. CaDiCaL_PriPro erhielt den Sonderinnovationspreis für seinen Beitrag zum schnellsten 2-Portfolio aller 48 teilnehmenden Solver.
