Model enumeration in propositional circumscription via unsatisfiable core analysis. (English) Zbl 1422.68217

Summary: Many practical problems are characterized by a preference relation over admissible solutions, where preferred solutions are minimal in some sense. For example, a preferred diagnosis usually comprises a minimal set of reasons that is sufficient to cause the observed anomaly. Alternatively, a minimal correction subset comprises a minimal set of reasons whose deletion is sufficient to eliminate the observed anomaly. Circumscription formalizes such preference relations by associating propositional theories with minimal models. The resulting enumeration problem is addressed here by means of a new algorithm taking advantage of unsatisfiable core analysis. Empirical evidence of the efficiency of the algorithm is given by comparing the performance of the resulting solver, {circumscriptino}, with {hclasp}, {camus_mcs}, {lbx} and {mcsls} on the enumeration of minimal models for problems originating from practical applications.


68T27 Logic in artificial intelligence
Full Text: DOI arXiv


[1] Alviano, M., Evaluating answer set programming with non-convex recursive aggregates, Fundamenta Informaticae, 149, 1-2, 1-34, (2016) · Zbl 1374.68096
[2] Alviano, M.; Calimeri, F.; Dodaro, C.; Fuscà, D.; Leone, N.; Perri, S.; Ricca, F.; Veltri, P.; Zangari, J.; Balduccini, M.; Janhunen, T., (2017)
[3] Alviano, M.; Dodaro, C.; Adorni, G.; Cagnoni, S.; Gori, M.; Maratea, M., (2016)
[4] Alviano, M.; Dodaro, C., Anytime answer set optimization via unsatisfiable core shrinking, Theory and Practice of Logic Programming, 16, 5-6, 533-551, (2016) · Zbl 1379.68033
[5] Alviano, M.; Dodaro, C.; Kambhampati, S., (2016)
[6] Alviano, M.; Dodaro, C.; Leone, N.; Ricca, F.; Calimeri, F.; Ianni, G.; Truszczynski, M., (2015)
[7] Alviano, M.; Dodaro, C.; Ricca, F.; Yang, Q.; Wooldridge, M., (2015)
[8] Alviano, M.; Faber, W.; Cabalar, P.; Son, T. C., (2013)
[9] Alviano, M.; Faber, W.; Gebser, M., Rewriting recursive aggregates in answer set programming: Back to monotonicity, Theory and Practice of Logic Programming, 15, 4-5, 559-573, (2015) · Zbl 1379.68034
[10] Alviano, M.; Leone, N., Complexity and compilation of GZ-aggregates in answer set programming, Theory and Practice of Logic Programming, 15, 4-5, 574-587, (2015) · Zbl 1379.68035
[11] Andres, B.; Kaufmann, B.; Matheis, O.; Schaub, T.; Dovier, A.; Costa, V. S., (2012)
[12] Audemard, G.; Simon, L.; Boutilier, C., (2009)
[13] Bacchus, F.; Narodytska, N.; Sinz, C.; Egly, U., (2014)
[14] Brewka, G.; Delgrande, J. P.; Romero, J.; Schaub, T.; Bonet, B.; Koenig, S., (2015)
[15] Brewka, G.; Delgrande, J. P.; Romero, J.; Schaub, T.; Calimeri, F.; Ianni, G.; Truszczynski, M., (2015)
[16] Dodaro, C.; Alviano, M.; Faber, W.; Leone, N.; Ricca, F.; Sirianni, M.; Fioravanti, F., (2011)
[17] Faber, W.; Vallati, M.; Cerutti, F.; Giacomin, M.; Kaminka, G. A.; Fox, M.; Bouquet, P.; Hüllermeier, E.; Dignum, V.; Dignum, F.; Van Harmelen, F., (2016)
[18] Gebser, M.; Kaminski, R.; Kaufmann, B.; Romero, J.; Schaub, T.; Calimeri, F.; Ianni, G.; Truszczynski, M., (2015)
[19] Gebser, M.; Kaminski, R.; Kaufmann, B.; Schaub, T.; Hill, P. M.; Warren, D. S., (2009)
[20] Gebser, M.; Kaminski, R.; Kaufmann, B.; Schaub, T., (2017)
[21] Gebser, M.; Kaufmann, B.; Neumann, A.; Schaub, T.; Baral, C.; Brewka, G.; Schlipf, J. S., (2007)
[22] Gebser, M.; Kaufmann, B.; Romero, J.; Otero, R.; Schaub, T.; Wanko, P.; Desjardins, M.; Littman, M. L., (2013)
[23] Gebser, M.; Kaufmann, B.; Schaub, T., Conflict-driven answer set solving: From theory to practice, Artificial Intelligence, 187, 52-89, (2012) · Zbl 1251.68060
[24] Giunchiglia, E.; Lierler, Y.; Maratea, M.; Mcguinness, D. L.; Ferguson, G., Proc. of 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, Sat-based answer set programming, 61-66, (2004), AAAI Press/MIT Press
[25] Giunchiglia, E.; Lierler, Y.; Maratea, M., Answer set programming based on propositional satisfiability, Journal of Automated Reasoning, 36, 4, 345-377, (2006) · Zbl 1107.68029
[26] Giunchiglia, E.; Maratea, M.; Fisher, M.; Van Der Hoek, W.; Konev, B.; Lisitsa, A., (2006)
[27] Janhunen, T.; Niemelä, I.; Balduccini, M.; Son, T. C., Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, Compact translations of non-disjunctive answer set programs to propositional clauses, 111-130, (2011), Springer · Zbl 1213.68025
[28] Jannach, D.; Schmitz, T.; Shchekotykhin, K. M., Parallel model-based diagnosis on multi-core computers, Journal of Artificial Intelligence Research, 55, 835-887, (2016) · Zbl 1352.68222
[29] Järvisalo, M.; Berre, D. L.; Roussel, O.; Simon, L., The international SAT solver competitions, AI Magazine, 33, 1, 89-94, (2012)
[30] Junker, U.; Mcguinness, D. L.; Ferguson, G., (2004)
[31] Kaminski, R.; Schaub, T.; Siegel, A.; Videla, S., Minimal intervention strategies in logical signaling networks with ASP, Theory and Practice of Logic Programming, 13, 4-5, 675-690, (2013) · Zbl 1286.68048
[32] Lee, J.; Lifschitz, V.; Palamidessi, C., (2003)
[33] Lee, J.; Lin, F., Loop formulas for circumscription, Artificial Intelligence, 170, 2, 160-185, (2006) · Zbl 1131.68105
[34] Leone, N.; Pfeifer, G.; Faber, W.; Eiter, T.; Gottlob, G.; Perri, S.; Scarcello, F., The DLV system for knowledge representation and reasoning, ACM Transactions on Computational Logic, 7, 3, 499-562, (2006) · Zbl 1367.68308
[35] Liffiton, M. H.; Sakallah, K. A., Algorithms for computing minimal unsatisfiable subsets of constraints, Journal of Automated Reasoning, 40, 1, 1-33, (2008) · Zbl 1154.68510
[36] Lifschitz, V., On the satisfiability of circumscription, Artificial Intelligence, 28, 1, 17-27, (1986) · Zbl 0589.03020
[37] Lin, F.; Zhao, Y., ASSAT: Computing answer sets of a logic program by SAT solvers, Artificial Intelligence, 157, 1-2, 115-137, (2004) · Zbl 1085.68544
[38] Marques-Silva, J.; Heras, F.; Janota, M.; Previti, A.; Belov, A.; Rossi, F., (2013)
[39] Marques-Silva, J.; Previti, A.; Sinz, C.; Egly, U., (2014)
[40] Mccarthy, J., Circumscription - A form of non-monotonic reasoning, Artificial Intelligence, 13, 1-2, 27-39, (1980) · Zbl 0435.68073
[41] Mencía, C.; Ignatiev, A.; Previti, A.; Marques-Silva, J.; Creignou, N.; Berre, D. L., (2016)
[42] Mencía, C.; Previti, A.; Marques-Silva, J.; Yang, Q.; Wooldridge, M., (2015)
[43] Morgado, A.; Heras, F.; Liffiton, M. H.; Planes, J.; Marques-Silva, J., Iterative and core-guided maxsat solving: A survey and assessment, Constraints, 18, 4, 478-534, (2013) · Zbl 1317.90199
[44] Narodytska, N.; Bacchus, F.; Brodley, C. E.; Stone, P., Proc. of 28th AAAI Conference on Artificial Intelligence, (2014)
[45] Pereira, L. M.; Damásio, C. V.; Alferes, J. J.; Fritszon, P., (1993)
[46] Romero, J.; Schaub, T.; Wanko, P.; Carro, M.; King, A.; Saeedloei, N.; Vos, M. D., (2016)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.