Abstract
Given a Satisfiability Modulo Theories (SMT) formula, a minimum satisfying assignment (MSA) is a partial assignment of minimum size that ensures the formula is satisfied. Minimum satisfying assignments find a number of practical applications that include software and hardware verification, among others. Recent work proposes the use of branch-and-bound search for computing MSAs. This paper proposes a novel counterexample-guided implicit hitting set approach for computing one MSA. Experimental results show significant performance gains over existing approaches.
Cite
CITATION STYLE
Ignatiev, A., Previti, A., & Marques-Silva, J. (2016). On finding minimum satisfying assignments. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9892 LNCS, pp. 287–297). Springer Verlag. https://doi.org/10.1007/978-3-319-44953-1_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
