Automated Software Analysis Group

Minimizing Models for Tseitin-Encoded SAT Instances

  • Author: Markus Iser, Carsten Sinz, Mana Taghdiri
  • 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}
}-