SAT’25 Test-of-Time Award

Our Effective Preprocessing in SAT through Variable and Clause Elimination paper presented at SAT’05 introduced efficient algorithms for Bounded Variable Elimination (BVA) preprocessing in SAT combined with subsumption, clause shrinking and gate extraction techniques:

Effective Preprocessing in SAT through Variable and Clause Elimination
Niklas Eén, Armin Biere
In Proc. 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'05), ,
vol. 3569, Springer 2005
[ paper | bibtex | doi | satelite | award ]

The approach is based on the Davies & Putnam clause distribution procedure and also builds on our predecessor work on eliminating existential variables in QBF.

It was was awarded the test-of-time award at SAT’25.