Home | Legals | Sitemap | KIT

Minimizing Models for Tseitin-Encoded SAT Instances

Minimizing Models for Tseitin-Encoded SAT Instances
Author: Markus Iser, Carsten Sinz, Mana Taghdiri links:
Place:

16th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2013 

Abstract:

Many applications of SAT solving can profit from minimal models—a partial variable assignment that is still a witness for satisfiability. Examples include software verification, model checking, and counterexample-guided abstraction refinement. In this paper, we examine how a given model can be minimized for SAT instances that have been obtained by Tseitin encoding of a full propositional logic formula. Our approach uses a SAT solver to efficiently minimize a given model, focusing on only the input variables. Experiments show that some models can be reduced by over 50 percent.

BibTex

@InProceedings{iser-sinz-taghdiri-sat2013,
    author    = {Markus Iser and Carsten Sinz and Mana Taghdiri},
    title     = {Minimizing Models for Tseitin-Encoded {SAT} Instances},
    booktitle = {16th International Conference on Theory and Applications of Satisfiability Testing (SAT)},
    pages     = {},
    year      = {2013},
    month     = {July}
}-