×

Improving MCS enumeration via caching. (English) Zbl 1496.68258

Gaspers, Serge (ed.) et al., Theory and applications of satisfiability testing – SAT 2017. 20th international conference, Melbourne, VIC, Australia, August 28 – September 1, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10491, 184-194 (2017).
Summary: Enumeration of minimal correction sets (MCSes) of conjunctive normal form formulas is a central and highly intractable problem in infeasibility analysis of constraint systems. Often complete enumeration of MCSes is impossible due to both high computational cost and worst-case exponential number of MCSes. In such cases partial enumeration is sought for, finding applications in various domains, including axiom pinpointing in description logics among others. In this work we propose caching as a means of further improving the practical efficiency of current MCS enumeration approaches, and show the potential of caching via an empirical evaluation.
For the entire collection see [Zbl 1368.68008].

MSC:

68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

sharpSAT; MiniSat; Chaff
PDFBibTeX XMLCite
Full Text: DOI Link