DOI: 10.2298/CSIS101019024Z

Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories

Jianmin Zhang1, Shengyu Shen1, Jun Zhang1 and Sikun Li1

  1. Dept. of Computer Science, National University of Defense Technology
    410073 Changsha, China
    {jmzhang,syshen,junzhang,wxxu,skli}@nudt.edu.cn

Abstract

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.

Key words

Satisfiability Modulo Theories, minimal unsatisfiable subformula, depth-first-search, breadth-first-search

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS101019024Z

Publication information

Volume 8, Issue 3 (June 2011)
Year of Publication: 2011
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Zhang, J., Shen, S., Zhang, J., Li, S.: Extracting Minimal Unsatisfiable Subformulas in Satisfiability Modulo Theories. Computer Science and Information Systems, Vol. 8, No. 3, 693-710. (2011), https://doi.org/10.2298/CSIS101019024Z