×

Minimal sets on propositional formulae. Problems and reductions. (English) Zbl 1419.68098

Summary: Boolean Satisfiability (SAT) is arguably the archetypical NP-complete decision problem. Progress in SAT solving algorithms has motivated an ever increasing number of practical applications in recent years. However, many practical uses of SAT involve solving function as opposed to decision problems. Concrete examples include computing minimal unsatisfiable subsets, minimal correction subsets, prime implicates and implicants, minimal models, backbone literals, and autarkies, among several others. In most cases, solving a function problem requires a number of adaptive or non-adaptive calls to a SAT solver. Given the computational complexity of SAT, it is therefore important to develop algorithms that either require the smallest possible number of calls to the SAT solver, or that involve simpler instances. This paper addresses a number of representative function problems defined on Boolean formulae, and shows that all these function problems can be reduced to a generic problem of computing a minimal set subject to a monotone predicate. This problem is referred to as the Minimal Set over Monotone Predicate (MSMP) problem. This work provides new ways for solving well-known function problems, including prime implicates, minimal correction subsets, backbone literals, independent variables and autarkies, among several others. Moreover, this work also motivates the development of more efficient algorithms for the MSMP problem. Finally the paper outlines a number of areas of future research related with extensions of the MSMP problem.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Ansótegui, C.; Bonet, M. L.; Levy, J., SAT-based MaxSAT algorithms, Artif. Intell., 196, 77-105 (2013) · Zbl 1270.68265
[2] Avidor, A.; Zwick, U., Approximating MIN 2-SAT and MIN 3-SAT, Theory Comput. Syst., 38, 329-345 (2005) · Zbl 1101.68603
[4] Bacchus, F.; Katsirelos, G., Using minimal correction sets to more efficiently compute minimal unsatisfiable sets, (Kroening, D.; Pasareanu, C. S., CAV (2015), Springer), 70-86
[5] Bailey, J.; Stuckey, P. J., Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization, (Hermenegildo, M. V.; Cabeza, D., PADL (2005), Springer), 174-186
[6] Bakker, R. R.; Dikker, F.; Tempelman, F.; Wognum, P. M., Diagnosing and solving over-determined constraint satisfaction problems, (Bajcsy, R., IJCAI (1993), Morgan Kaufmann), 276-281
[8] Belov, A.; Ivrii, A.; Matsliah, A.; Marques-Silva, J., On efficient computation of variable MUSes, (Cimatti, A.; Sebastiani, R., SAT (2012), Springer), 298-311 · Zbl 1273.03047
[9] Belov, A.; Janota, M.; Lynce, I.; Marques-Silva, J., On computing minimal equivalent subformulas, (Milano, M., CP (2012), Springer), 158-174
[10] Belov, A.; Janota, M.; Lynce, I.; Marques-Silva, J., Algorithms for computing minimal equivalent subformulas, Artif. Intell., 216, 309-326 (2014) · Zbl 1405.68340
[11] Belov, A.; Lynce, I.; Marques-Silva, J., Towards efficient MUS extraction, AI Commun., 25, 97-116 (2012) · Zbl 1248.68450
[12] Belov, A.; Marques-Silva, J., Minimally unsatisfiable Boolean circuits, (Sakallah, K. A.; Simon, L., SAT (2011), Springer), 145-158 · Zbl 1330.68268
[13] Ben-Eliyahu, R.; Dechter, R., On computing minimal models, Ann. Math. Artif. Intell., 18, 3-27 (1996) · Zbl 0891.68109
[14] Ben-Eliyahu-Zohary, R.; Palopoli, L., Reasoning with minimal models: efficient algorithms and applications, Artif. Intell., 96, 421-449 (1997) · Zbl 0903.68178
[15] Bentley, J. L.; Yao, A. C., An almost optimal algorithm for unbounded searching, Inf. Process. Lett., 5, 82-87 (1976) · Zbl 0335.68030
[17] Besnard, P.; Grégoire, É.; Piette, C.; Raddaoui, B., MUS-based generation of arguments and counter-arguments, (IRI (2010), IEEE Systems, Man, and Cybernetics Society), 239-244
[18] Bessiere, C.; Fargier, H.; Lecoutre, C., Global inverse consistency for interactive constraint satisfaction, (Schulte, C., CP (2013), Springer), 159-174
[19] Biere, A., PicoSAT essentials, JSAT, 4, 75-97 (2008) · Zbl 1159.68403
[20] (Biere, A.; Heule, M.; van Maarenaum, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in AI and Applications, vol. 185 (2009), IOS Press) · Zbl 1183.68568
[21] Birnbaum, E.; Lozinskii, E. L., Consistent subsets of inconsistent systems: structure and behaviour, J. Exp. Theor. Artif. Intell., 15, 25-46 (2003) · Zbl 1025.68090
[22] (Bonet, B.; Koenig, S., Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA (2015), AAAI Press)
[23] Bossu, G.; Siegel, P., Saturation, nonmonotonic reasoning and the closed-world assumption, Artif. Intell., 25, 13-63 (1985) · Zbl 0569.68078
[24] Boufkhad, Y.; Roussel, O., Redundancy in random SAT formulas, (Kautz, H. A.; Porter, B. W., AAAI/IAAI (2000), AAAI Press/The MIT Press), 273-278
[25] Bradley, A. R.; Manna, Z., Checking safety by inductive generalization of counterexamples to induction, (FMCAD (2007), IEEE Press), 173-180
[26] Bradley, A. R.; Manna, Z., Property-directed incremental invariant generation, Form. Asp. Comput., 20, 379-405 (2008) · Zbl 1149.68402
[27] (Brodley, C. E.; Stone, P., Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27-31, 2014, Québec City, Québec, Canada (2014), AAAI Press)
[28] Brown, F. M., Boolean Reasoning: The Logic of Boolean Equations (1990), Springer · Zbl 0719.03002
[29] Buss, S. R.; Krajíček, J.; Takeuti, G., Provably total functions in the bounded arithmetic theories \(R_3^i, U_2^i\), and \(V_2^i\), (Clote, P.; Krajíček, J., Arithmetic, Proof Theory, and Computational Complexity (1995), OUP), 116-161
[30] Castell, T., Computation of prime implicates and prime implicants by a variant of the Davis and Putnam procedure, (ICTAI (1996), IEEE Computer Society), 428-429
[31] Chakraborty, S.; Meel, K. S.; Vardi, M. Y., Balancing scalability and uniformity in SAT witness generator, (DAC (2014), ACM), 60:1-60:6
[32] Chen, Z. Z.; Toda, S., The complexity of selecting maximal solutions, (Structure in Complexity Theory Conference (1993), IEEE Computer Society), 313-325
[33] Chen, Z. Z.; Toda, S., The complexity of selecting maximal solutions, Inf. Comput., 119, 231-239 (1995) · Zbl 0834.68045
[34] Chinneck, J. W.; Dravnieks, E. W., Locating minimal infeasible constraint sets in linear programs, INFORMS J. Comput., 3, 157-168 (1991) · Zbl 0755.90055
[35] Chmeiss, A.; Krawczyk, V.; Sais, L., Redundancy in CSPs, (Ghallab, M.; Spyropoulos, C. D.; Fakotakis, N.; Avouris, N. M., ECAI (2008), IOS Press), 907-908
[36] Codish, M.; Fekete, Y.; Metodi, A., Backbones for equality, (Bertacco, V.; Legay, A., Haifa Verification Conference (2013), Springer), 1-14
[37] Crama, Y.; Hammer, P. L., Boolean Functions - Theory, Algorithms, and Applications, Encyclopedia of Mathematics and Its Applications, vol. 142 (2011), Cambridge University Press · Zbl 1237.06001
[38] Darwiche, A.; Marquis, P., A knowledge compilation map, J. Artif. Intell. Res., 17, 229-264 (2002) · Zbl 1045.68131
[39] Déharbe, D.; Fontaine, P.; Berre, D. L.; Mazure, B., Computing prime implicants, (FMCAD (2013), IEEE), 46-52
[40] Desrosiers, C.; Galinier, P.; Hertz, A.; Paroz, S., Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, J. Comb. Optim., 18, 124-150 (2009) · Zbl 1173.90510
[41] Dietmeyer, D. L.; Schneider, P. R., Identification of symmetry, redundancy and equivalence of Boolean functions, IEEE Trans. Electron. Comput., EC-16, 804-817 (1967) · Zbl 0183.18702
[43] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., SAT (2003), Springer), 502-518 · Zbl 1204.68191
[44] Eén, N.; Sörensson, N., Translating pseudo-Boolean constraints into SAT, JSAT, 2, 1-26 (2006) · Zbl 1116.68083
[45] Eiter, T.; Gottlob, G., Propositional circumscription and extended closed-world reasoning are \(\Pi_2^P\)-complete, Theor. Comput. Sci., 114, 231-245 (1993) · Zbl 0786.68085
[46] Eiter, T.; Gottlob, G., The complexity of logic-based abduction, J. ACM, 42, 3-42 (1995) · Zbl 0886.68121
[47] Felfernig, A.; Schubert, M.; Zehentner, C., An efficient diagnosis algorithm for inconsistent constraint sets, Artif. Intell. Eng. Des. Anal. Manuf., 26, 53-62 (2012)
[48] Garey, M. R.; Johnson, D. S., Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), W. H. Freeman · Zbl 0411.68039
[49] Grégoire, É.; Lagniez, J., On anti-subsumptive knowledge enforcement, (LPAR (2015)), 48-62 · Zbl 1471.68271
[51] Grégoire, É.; Lagniez, J.; Mazure, B., Multiple contraction through Partial-Max-SAT, (ICTAI (2014), IEEE Computer Society), 321-327
[52] Grégoire, É.; Mazure, B.; Piette, C., On approaches to explaining infeasibility of sets of Boolean clauses, (ICTAI (1) (2008), IEEE Computer Society), 74-83
[53] Gupta, A., Learning Abstractions for Model Checking (2006), Carnegie Mellon University, Ph.D. thesis
[54] Gurfinkel, A.; Belov, A.; Marques-Silva, J., Synthesizing safe bit-precise invariants, (Ábrahám, E.; Havelund, K., Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8413 (2014), Springer), 93-108
[55] Hemery, F.; Lecoutre, C.; Sais, L.; Boussemart, F., Extracting MUCs from constraint networks, (Brewka, G.; Coradeschi, S.; Perini, A.; Traverso, P., ECAI (2006), IOS Press), 113-117
[56] Heras, F.; Morgado, A.; Marques-Silva, J., An empirical study of encodings for group MaxSAT, (Kosseim, L.; Inkpen, D., Canadian Conference on AI (2012), Springer), 85-96
[57] Heras, F.; Morgado, A.; Marques-Silva, J., MaxSAT-based encodings for group MaxSAT, AI Commun., 28, 195-214 (2015) · Zbl 1373.68377
[58] (Heule, M.; Weaver, S., SAT. SAT, Lecture Notes in Computer Science, vol. 9340 (2015), Springer)
[59] Hyttinen, A.; Hoyer, P. O.; Eberhardt, F.; Järvisalo, M., Discovering cyclic causal models with latent variables: a general sat-based procedure, (UAI (2013))
[61] Ignatiev, A.; Morgado, A.; Marques-Silva, J., On reducing maximum independent set to minimum satisfiability, (Sinz, C.; Egly, U., SAT (2014), Springer), 103-120 · Zbl 1423.68452
[62] Ignatiev, A.; Morgado, A.; Planes, J.; Marques-Silva, J., Maximal falsifiability - definitions, algorithms, and applications, (McMillan, K. L.; Middeldorp, A.; Voronkov, A., LPAR (2013), Springer), 439-456 · Zbl 1407.68453
[63] Ignatiev, A.; Previti, A.; Liffiton, M. H.; Marques-Silva, J., Smallest MUS extraction with minimal hitting set dualization, (CP (2015)), 173-182
[65] Ivrii, A.; Malik, S.; Meel, K. S.; Vardi, M. Y., On computing minimal independent support and its applications to sampling and counting, Constraints, 21, 1, 41-58 (2016) · Zbl 1334.90146
[66] Jabbour, S.; Marques-Silva, J.; Sais, L.; Salhi, Y., Enumerating prime implicants of propositional formulae in conjunctive normal form, (Fermé, E.; Leite, J., JELIA (2014), Springer), 152-165 · Zbl 1432.68327
[67] Janota, M., Do SAT solvers make good configurators?, (Thiel, S.; Pohl, K., SPLC (2) (2008), Lero Int. Science Centre, University of Limerick: Lero Int. Science Centre, University of Limerick Ireland), 191-195
[68] Janota, M.; Botterweck, G.; Marques-Silva, J., On lazy and eager interactive reconfiguration, (Proceedings of the 8th International Workshop on Variability Modelling of Software-Intensive Systems. Proceedings of the 8th International Workshop on Variability Modelling of Software-Intensive Systems, VaMoS (2014), ACM), 8:1-8:8
[69] Janota, M.; Lynce, I.; Marques-Silva, J., Algorithms for computing backbones of propositional formulae, AI Commun., 28, 161-177 (2015) · Zbl 1373.68379
[70] Janota, M.; Marques-Silva, J., On the query complexity of selecting minimal sets for monotone predicates, Artif. Intell., 233, 73-83 (2016) · Zbl 1351.68117
[71] Jose, M.; Majumdar, R., Bug-assist: assisting fault localization in ANSI-C programs, (Gopalakrishnan, G.; Qadeer, S., CAV (2011), Springer), 504-509
[72] Jose, M.; Majumdar, R., Cause clue clauses: error localization using maximum satisfiability, (Hall, M. W.; Padua, D. A., PLDI (2011), ACM), 437-446
[73] Junker, U., QuickXplain: preferred explanations and relaxations for over-constrained problems, (McGuinness, D. L.; Ferguson, G., AAAI (2004), AAAI Press/The MIT Press), 167-172
[74] Kaiser, A.; Küchlin, W., Detecting inadmissible and necessary variables in large propositional formulae, (Intl. Joint Conf. on Automated Reasoning (Short Papers) (2001))
[75] Kavvadias, D. J.; Sideri, M.; Stavropoulos, E. C., Generating all maximal models of a Boolean expression, Inf. Process. Lett., 74, 157-162 (2000) · Zbl 1339.03015
[76] Kilby, P.; Slaney, J. K.; Thiébaux, S.; Walsh, T., Backbones and backdoors in satisfiability, (Veloso, M. M.; Kambhampati, S., AAAI (2005), AAAI Press/The MIT Press), 1368-1373
[77] de Kleer, J., An improved incremental algorithm for generating prime implicates, (Swartout, W. R., AAAI (1992), AAAI Press/The MIT Press), 780-785
[79] Kleine Büning, H.; Letterman, T., Propositional Logic: Deduction and Algorithms (1999), Cambridge University Press · Zbl 0957.03001
[80] Kohli, R.; Krishnamurti, R.; Mirchandani, P., The minimum satisfiability problem, SIAM J. Discrete Math., 7, 275-283 (1994) · Zbl 0806.68060
[82] Koshimura, M.; Nabeshima, H.; Fujita, H.; Hasegawa, R., Minimal model generation with respect to an atom set, (FTP (2009)), 49-59
[83] Krentel, M. W., The complexity of optimization problems, J. Comput. Syst. Sci., 36, 490-509 (1988) · Zbl 0652.68040
[84] Kullmann, O., Investigations on autark assignments, Discrete Appl. Math., 107, 99-137 (2000) · Zbl 0965.03018
[85] Kullmann, O., On the use of autarkies for satisfiability decision, Electron. Notes Discrete Math., 9, 231-253 (2001) · Zbl 0990.90545
[86] Kullmann, O., Constraint satisfaction problems in clausal form I: autarkies and deficiency, Fundam. Inform., 109, 27-81 (2011) · Zbl 1242.68289
[87] Kullmann, O., Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure, Fundam. Inform., 109, 83-119 (2011) · Zbl 1242.68290
[88] Kullmann, O.; Lynce, I.; Marques-Silva, J., Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel, (Biere, A.; Gomes, C. P., SAT (2006), Springer), 22-35 · Zbl 1187.68552
[91] Lang, J.; Liberatore, P.; Marquis, P., Propositional independence: formula-variable independence and forgetting, J. Artif. Intell. Res., 18, 391-443 (2003) · Zbl 1056.68112
[93] Li, C. M.; Zhu, Z.; Manyà, F.; Simon, L., Optimizing with minimum satisfiability, Artif. Intell., 190, 32-44 (2012) · Zbl 1251.68209
[94] Liberatore, P., Redundancy in logic I: CNF propositional formulae, Artif. Intell., 163, 203-232 (2005) · Zbl 1132.68736
[95] Liberatore, P., Redundancy in logic II: 2CNF and Horn propositional formulae, Artif. Intell., 172, 265-299 (2008) · Zbl 1182.68282
[96] Liberatore, P., Redundancy in logic III: non-monotonic reasoning, Artif. Intell., 172, 1317-1359 (2008) · Zbl 1183.68598
[97] Liffiton, M. H.; Malik, A., Enumerating infeasibility: finding multiple MUSes quickly, (Gomes, C. P.; Sellmann, M., CPAIOR (2013), Springer), 160-175 · Zbl 1382.68226
[98] Liffiton, M. H.; Previti, A.; Malik, A.; Marques-Silva, J., Fast, flexible MUS enumeration, Constraints, 21, 2, 223-250 (2016) · Zbl 1334.90080
[99] Liffiton, M. H.; Sakallah, K. A., Algorithms for computing minimal unsatisfiable subsets of constraints, J. Autom. Reason., 40, 1-33 (2008) · Zbl 1154.68510
[100] Liffiton, M. H.; Sakallah, K. A., Searching for autarkies to trim unsatisfiable clause sets, (Kleine Büning, H.; Zhao, X., SAT (2008), Springer), 182-195 · Zbl 1138.68545
[101] Marathe, M. V.; Ravi, S. S., On approximation algorithms for the minimum satisfiability problem, Inf. Process. Lett., 58, 23-29 (1996) · Zbl 0875.68544
[102] Marques-Silva, J., Computing minimally unsatisfiable subformulas: state of the art and future directions, J. Mult.-Valued Log. Soft Comput., 19, 163-183 (2012) · Zbl 1394.68359
[103] Marques-Silva, J.; Heras, F.; Janota, M.; Previti, A.; Belov, A., On computing minimal correction subsets, (Rossi, F., IJCAI (2013), IJCAI/AAAI)
[105] Marques-Silva, J.; Janota, M., Computing minimal sets on propositional formulae I: problems & reductions (2014), CoRR
[106] Marques-Silva, J.; Janota, M., On the query complexity of selecting few minimal sets, Electron. Colloq. Comput. Complex., 21, 31 (2014)
[108] Marques-Silva, J.; Janota, M.; Lynce, I., On computing backbones of propositional theories, (Coelho, H.; Studer, R.; Wooldridge, M., ECAI (2010), IOS Press), 15-20 · Zbl 1211.68389
[109] Marques-Silva, J.; Lynce, I., On improving MUS extraction algorithms, (Sakallah, K. A.; Simon, L., SAT (2011), Springer), 159-173 · Zbl 1330.68273
[111] Marquis, P., Consequence finding algorithms, (Gabbay, D. M.; Smets, P., Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol. 5 (2000), Springer), 41-145, Chap. 3 · Zbl 1015.68197
[112] McCluskey, E., Minimization of Boolean functions, Bell Labs Tech. J., 35, 1417-1444 (1956)
[113] Mencía, C.; Ignatiev, A.; Previti, A.; Marques-Silva, J., MCS extraction with sublinear oracle queries, (Creignou, N.; Berre, D. L., Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing. Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France, July 5-8, 2016 (2016), Springer), 342-360 · Zbl 1475.68220
[115] Monasson, R.; Zecchina, R.; Kirkpatrick, S.; Selman, B.; Troyansky, L., 2+p-SAT: relation of typical-case complexity to the nature of the phase transition, Random Struct. Algorithms, 15, 414-435 (1999) · Zbl 0931.68056
[116] Monien, B.; Speckenmeyer, E., Solving satisfiability in less than \(2^n\) steps, Discrete Appl. Math., 10, 287-295 (1985) · Zbl 0603.68092
[117] Morgado, A.; Heras, F.; Liffiton, M. H.; Planes, J.; Marques-Silva, J., Iterative and core-guided MaxSAT solving: a survey and assessment, Constraints, 18, 478-534 (2013) · Zbl 1317.90199
[118] Nadel, A., Boosting minimal unsatisfiable core extraction, (Bloem, R.; Sharygina, N., FMCAD (2010), IEEE), 221-229
[119] Niemelä, I., A tableau calculus for minimal model reasoning, (Miglioli, P.; Moscato, U.; Mundici, D.; Ornaghi, M., TABLEAUX (1996), Springer), 278-294 · Zbl 1412.68247
[120] Nöhrer, A.; Biere, A.; Egyed, A., Managing SAT inconsistencies with HUMUS, (Eisenecker, U. W.; Apel, S.; Gnesi, S., VaMoS (2012), ACM), 83-91
[121] Papadimitriou, C. H., Computational Complexity (1994), Addison Wesley · Zbl 0557.68033
[122] Plaisted, D. A.; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 293-304 (1986) · Zbl 0636.68119
[125] Previti, A.; Marques-Silva, J., Partial MUS enumeration, (desJardins, M.; Littman, M. L., AAAI (2013), AAAI Press)
[126] Pritchard, P., Opportunistic algorithms for eliminating supersets, Acta Inform., 28, 733-754 (1991) · Zbl 0724.68045
[127] Quine, W. V., A way to simplify truth functions, Am. Math. Mon., 62, 627-631 (1955) · Zbl 0068.24209
[128] Ravi, K.; Somenzi, F., Minimal assignments for bounded model checking, (Jensen, K.; Podelski, A., TACAS (2004), Springer), 31-45 · Zbl 1126.68486
[129] Reiter, R., A theory of diagnosis from first principles, Artif. Intell., 32, 57-95 (1987) · Zbl 0643.68122
[130] Reiter, R.; de Kleer, J., Foundations of assumption-based truth maintenance systems: preliminary report, (Forbus, K. D.; Shrobe, H. E., AAAI (1987), Morgan Kaufmann), 183-189
[131] Rosa, E. D.; Giunchiglia, E.; Maratea, M., Solving satisfiability problems with preferences, Constraints, 15, 485-515 (2010) · Zbl 1208.68199
[132] Roussel, O.; Manquinho, V. M., Pseudo-Boolean and cardinality constraints, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Front. Artif. Intell. Appl., vol. 185 (2009), IOS Press), 695-733 · Zbl 1183.68568
[133] Safarpour, S.; Mangassarian, H.; Veneris, A. G.; Liffiton, M. H.; Sakallah, K. A., Improved design debugging using maximum satisfiability, (FMCAD (2007), IEEE Computer Society), 13-19
[134] (Schaub, T.; Friedrich, G.; O’Sullivan, B., ECAI 2014 - 21st European Conference on Artificial Intelligence. ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems, PAIS 2014. ECAI 2014 - 21st European Conference on Artificial Intelligence. ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems, PAIS 2014, Front. Artif. Intell. Appl., vol. 263 (2014), IOS Press) · Zbl 1296.68011
[135] (Sharygina, N.; Veith, H., Computer Aided Verification. Computer Aided Verification, CAV. Computer Aided Verification. Computer Aided Verification, CAV, Lecture Notes in Computer Science, vol. 8044 (2013), Springer) · Zbl 1268.68032
[136] Shen, S.; Qin, Y.; Li, S., A faster counterexample minimization algorithm based on refutation analysis, (DATE (2005), IEEE Computer Society), 672-677
[137] Shen, S.; Qin, Y.; Li, S., Minimizing counterexample with unit core extraction and incremental SAT, (Cousot, R., VMCAI (2005), Springer), 298-312 · Zbl 1111.68515
[138] Sinz, C.; Kaiser, A.; Küchlin, W., Detection of inconsistencies in complex product configuration data using extended propositional SAT-checking, (Russell, I.; Kolen, J. F., FLAIRS Conference (2001), AAAI Press), 645-649
[139] Sinz, C.; Kaiser, A.; Küchlin, W., Formal methods for the validation of automotive product configuration data, Artif. Intell. Eng. Des. Anal. Manuf., 17, 75-97 (2003)
[140] de Siqueira, J. L.N.; Puget, J. F., Explanation-based generalisation of failures, (ECAI (1988)), 339-344
[142] Slaney, J. K.; Walsh, T., Backbones in optimization and approximation, (Nebel, B., IJCAI (2001), Morgan Kaufmann), 254-259
[143] Soh, T.; Inoue, K., Identifying necessary reactions in metabolic pathways by minimal model generation, (Coelho, H.; Studer, R.; Wooldridge, M., ECAI (2010), IOS Press), 277-282 · Zbl 1211.92025
[144] Straach, J.; Truemper, K., Learning to ask relevant questions, Artif. Intell., 111, 301-327 (1999) · Zbl 0996.68199
[145] To, S. T.; Son, T. C.; Pontelli, E., Conjunctive representations in contingent planning: prime implicates versus minimal CNF formula, (Burgard, W.; Roth, D., AAAI (2011), AAAI Press)
[146] Tseitin, G. S., On the complexity of derivation in propositional calculus, (Studies in Constructive Mathematics and Mathematical Logic, Part II (1968)), 115-125 · Zbl 0197.00102
[147] Umans, C.; Villa, T.; Sangiovanni-Vincentelli, A. L., Complexity of two-level logic minimization, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 25, 1230-1246 (2006)
[148] Van Gelder, A., Autarky pruning in propositional model elimination reduces failure redundancy, J. Autom. Reason., 23, 137-193 (1999) · Zbl 0939.68108
[149] Van Gelder, A., Complexity analysis of propositional resolution with autarky pruning, Discrete Appl. Math., 96-97, 195-221 (1999) · Zbl 0937.68150
[150] Vesic, S., Identifying the class of maxi-consistent operators in argumentation, J. Artif. Intell. Res., 47, 71-93 (2013) · Zbl 1276.68143
[151] Wallner, J. P.; Weissenbacher, G.; Woltran, S., Advanced SAT techniques for abstract argumentation, (Leite, J.; Son, T. C.; Torroni, P.; van der Torre, L.; Woltran, S., CLIMA (2013), Springer), 138-154 · Zbl 1401.68312
[152] Wieringa, S., Understanding, improving and parallelizing MUS finding using model rotation, (Milano, M., CP (2012), Springer), 672-687
[153] (Yang, Q.; Wooldridge, M., Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015 (2015), AAAI Press)
[154] Zeller, A., Yesterday, my program worked. Today, it does not. Why?, (Nierstrasz, O.; Lemoine, M., ESEC/SIGSOFT FSE (1999), Springer), 253-267
[155] Zhang, J.; Shen, S.; Zhang, J.; Xu, W.; Li, S., Extracting minimal unsatisfiable subformulas in satisfiability modulo theories, Comput. Sci. Inf. Syst., 8, 693-710 (2011)
[156] Zhu, C. S.; Weissenbacher, G.; Malik, S., Post-silicon fault localisation using maximum satisfiability and backbones, (Bjesse, P.; Slobodová, A., FMCAD (2011), FMCAD Inc.), 63-66
[157] Zhu, C. S.; Weissenbacher, G.; Sethi, D.; Malik, S., SAT-based techniques for determining backbones for post-silicon fault localisation, (Zilic, Z.; Shukla, S. K., HLDVT (2011), IEEE), 84-91
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.