Geodesic
Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories
Computer Science and Information Systems, Tome 8 (2011) no. 3.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

Explaining the causes of infeasibility of formulas has practical applications in various fields, such as formal verification and electronic design automation. A minimal unsatisfiable subformula provides a succinct explanation of infeasibility and is valuable for applications. The problem of deriving minimal unsatisfiable cores from Boolean formulas has been addressed rather frequently in recent years. However little attention has been concentrated on extraction of unsatisfiable subformulas in Satisfiability Modulo Theories(SMT). In this paper, we propose a depth-firstsearch algorithm and a breadth-first-search algorithm to compute minimal unsatisfiable cores in SMT, adopting different searching strategy. We report and analyze experimental results obtaining from a very extensive test on SMT-LIB benchmarks.
Keywords: Satisfiability Modulo Theories, minimal unsatisfiable subformula, depth-first-search, breadth-first-search 
@article{CSIS_2011_8_3_a9,
     author = {Jianmin Zhang and Shengyu Shen and Jun Zhang and Sikun Li},
     title = {Extracting {Minimal} {Unsatisfiable} {Subformulas} in {Satisfiability} {Modulo} {Theories}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {8},
     number = {3},
     year = {2011},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2011_8_3_a9/}
}
TY  - JOUR
AU  - Jianmin Zhang
AU  - Shengyu Shen
AU  - Jun Zhang
AU  - Sikun Li
TI  - Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories
JO  - Computer Science and Information Systems
PY  - 2011
VL  - 8
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2011_8_3_a9/
ID  - CSIS_2011_8_3_a9
ER  - 
%0 Journal Article
%A Jianmin Zhang
%A Shengyu Shen
%A Jun Zhang
%A Sikun Li
%T Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories
%J Computer Science and Information Systems
%D 2011
%V 8
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2011_8_3_a9/
%F CSIS_2011_8_3_a9
Jianmin Zhang; Shengyu Shen; Jun Zhang; Sikun Li. Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories. Computer Science and Information Systems, Tome 8 (2011) no. 3. http://geodesic.mathdoc.fr/item/CSIS_2011_8_3_a9/