CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Effective preprocessing in SAT through variable and clause elimination

Niklas Een (Institutionen för data- och informationsteknik (Chalmers)) ; A. Biere
Lecture Notes in Computer Science (0302-9743). Vol. 3569 (2005), p. 61-75.
[Artikel, refereegranskad vetenskaplig]

Preprocessing SAT instances can reduce their size considerably. We combine variable elimination with subsumption and self-subsuming resolution, and show that these techniques not only shrink the formula further than previous preprocessing efforts based on variable elimination, but also decrease runtime of SAT solvers substantially for typical industrial SAT problems. We discuss critical implementation details that make the reduction procedure fast enough to be practical.

8th International Conference on Theory and Applications of Satisfiability Testing, Jun 19-23, 2005, S:t Andrews, Scotland

Denna post skapades 2010-02-25.
CPL Pubid: 115015


Institutioner (Chalmers)

Institutionen för data- och informationsteknik (Chalmers)


Datavetenskap (datalogi)

Chalmers infrastruktur