@inproceedings{JarvisaloB:SAT2010, author = {Matti J\"arvisalo and Armin Biere}, title = {Reconstructing Solutions after Blocked Clause Elimination}, editor = {Ofer Strichman and Stefan Szeider}, booktitle = {Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6175}, pages = {340--345}, year = {2010}, } Abstract: Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to extract a full satisfying assignment for original SAT instances from a satisfying assignment for the instances after preprocessing. We show how such full solutions can be efficiently reconstructed from solutions to the conjunctive normal form (CNF) formulas resulting from applying a combination of various CNF preprocessing techniques implemented in the PrecoSAT solver—especially, blocked clause elimination combined with SatElite-style variable elimination and equivalence reasoning.