×

Algorithms for computing minimal equivalent subformulas. (English) Zbl 1405.68340

Summary: Knowledge representation and reasoning using propositional logic is an important component of AI systems. A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses – clauses whose removal from the formula does not affect the set of its models. Identification of redundant clauses is important because redundancy often leads to unnecessary computation, wasted storage, and may obscure the structure of the problem. A formula obtained by the removal of all redundant clauses from a given CNF formula \(\mathcal{F}\) is called a Minimal Equivalent Subformula (MES) of \(\mathcal{F}\). This paper proposes a number of efficient algorithms and optimization techniques for the computation of MESes. Previous work on MES computation proposes a simple algorithm based on iterative application of the definition of a redundant clause, similar to the well-known deletion-based approach for the computation of Minimal Unsatisfiable Subformulas (MUSes). This paper observes that, in fact, most of the existing algorithms for the computation of MUSes can be adapted to the computation of MESes. However, some of the optimization techniques that are crucial for the performance of the state-of-the-art MUS extractors cannot be applied in the context of MES computation, and thus the resulting algorithms are often not efficient in practice. To address the problem of efficient computation of MESes, the paper develops a new class of algorithms that are based on the iterative analysis of subsets of clauses, and a lightweight pruning technique based on the computation of backbones. The experimental results, obtained on representative problem instances, confirm the effectiveness of the proposed methods. The experimental results also reveal that many CNF instances obtained from the practical applications of SAT exhibit a large degree of redundancy.

MSC:

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

References:

[1] Darwiche, A.; Marquis, P., A knowledge compilation map, J. Artif. Intell. Res., 17, 229-264 (2002) · Zbl 1045.68131
[2] Liberatore, P., Redundancy in logic I: CNF propositional formulae, Artif. Intell., 163, 2, 203-232 (2005) · Zbl 1132.68736
[3] Boufkhad, Y.; Roussel, O., Redundancy in random SAT formulas, (AAAI (2000)), 273-278
[4] Grégoire, É.; Mazure, B.; Piette, C., On approaches to explaining infeasibility of sets of Boolean clauses, (ICTAI (2008)), 74-83
[5] Desrosiers, C.; Galinier, P.; Hertz, A.; Paroz, S., Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, J. Comb. Optim., 18, 2, 124-150 (2009) · Zbl 1173.90510
[6] Marques-Silva, J., Minimal unsatisfiability: models, algorithms and applications, (ISMVL (2010)), 9-14
[8] Pipatsrisawat, K.; Darwiche, A., On the power of clause-learning SAT solvers as resolution engines, Artif. Intell., 175, 2, 512-525 (2011) · Zbl 1216.68235
[9] Atserias, A.; Fichte, J. K.; Thurley, M., Clause-learning algorithms with many restarts and bounded-width resolution, J. Artif. Intell. Res., 40, 353-373 (2011) · Zbl 1214.68340
[10] 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), 1023-1028
[11] To, S. T.; Son, T. C.; Pontelli, E., On the use of prime implicates in conformant planning, (Fox, M.; Poole, D., AAAI Conference on Artificial Intelligence (2010), AAAI Press), 1205-1210
[12] Niepert, M.; Gucht, D. V.; Gyssens, M., Logical and algorithmic properties of stable conditional independence, Int. J. Approx. Reason., 51, 5, 531-543 (2010) · Zbl 1205.68428
[14] Lonsing, F.; Biere, A., Failed literal detection for QBF, (Sakallah, K. A.; Simon, L., SAT, vol. 6695 (2011), Springer), 259-272 · Zbl 1330.68118
[15] Biere, A.; Lonsing, F.; Seidl, M., Blocked clause elimination for QBF, (Bjørner, N.; Sofronie-Stokkermans, V., CADE (2011), Springer), 101-115 · Zbl 1341.68181
[16] Dechter, A.; Dechter, R., Removing redundancies in constraint networks, (Forbus, K. D.; Shrobe, H. E., AAAI (1987)), 105-109
[17] Choi, C. W.; Lee, J. H.-M.; Stuckey, P. J., Removing propagation redundant constraints in redundant modeling, ACM Trans. Comput. Log., 8, 4 (2007) · Zbl 1367.68262
[18] Chmeiss, A.; Krawczyk, V.; Sais, L., Redundancy in CSPs, (ECAI (2008)), 907-908
[19] Scholl, C.; Disch, S.; Pigorsch, F.; Kupferschmid, S., Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints, (Kowalewski, S.; Philippou, A., TACAS (2009)), 383-397 · Zbl 1234.68266
[20] Grimm, S.; Wissmann, J., Elimination of redundancy in ontologies, (ESWC (2011)), 260-274
[21] Dershowitz, N.; Hanna, Z.; Nadel, A., A scalable algorithm for minimal unsatisfiable core extraction, (SAT (2006)), 36-41 · Zbl 1187.68538
[22] Nadel, A., Boosting minimal unsatisfiable core extraction, (FMCAD (2010)), 121-128
[23] Marques-Silva, J.; Lynce, I., On improving MUS extraction algorithms, (SAT (2011)), 159-173 · Zbl 1330.68273
[24] Belov, A.; Marques-Silva, J., Accelerating MUS extraction with recursive model rotation, (FMCAD (2011)), 37-40
[25] Liffiton, M. H.; Sakallah, K. A., Algorithms for computing minimal unsatisfiable subsets of constraints, J. Autom. Reason., 40, 1, 1-33 (2008) · Zbl 1154.68510
[27] Plaisted, D. A.; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304 (1986) · Zbl 0636.68119
[28] (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press) · Zbl 1183.68568
[29] Chinneck, J. W.; Dravnieks, E. W., Locating minimal infeasible constraint sets in linear programs, INFORMS J. Comput., 3, 2, 157-168 (1991) · Zbl 0755.90055
[30] Bakker, R. R.; Dikker, F.; Tempelman, F.; Wognum, P. M., Diagnosing and solving over-determined constraint satisfaction problems, (IJCAI (1993)), 276-281
[31] Siqueira N., J. L.; Puget, J.-F., Explanation-based generalisation of failures, (ECAI (1988)), 339-344
[32] Hemery, F.; Lecoutre, C.; Sais, L.; Boussemart, F., Extracting MUCs from constraint networks, (ECAI (2006)), 113-117
[33] Junker, U., QuickXplain: preferred explanations and relaxations for over-constrained problems, (AAAI (2004)), 167-172
[34] Marques-Silva, J.; Janota, M.; Belov, A., Minimal sets over monotone predicates in boolean formulae, (Sharygina, N.; Veith, H., CAV (2013), Springer), 592-607
[35] Kullmann, O., Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure, Fundam. Inform., 109, 1, 83-119 (2011) · Zbl 1242.68290
[38] Belov, A.; Lynce, I.; Marques-Silva, J., Towards efficient MUS extraction, AI Commun., 25, 2, 97-116 (2012) · Zbl 1248.68450
[39] Biere, A., Picosat essentials, J. Satisf. Boolean Model. Comput., 4, 2-4, 75-97 (2008) · Zbl 1159.68403
[40] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., SAT (2003), Springer), 502-518 · Zbl 1204.68191
[41] Eén, N.; Sörensson, N., Temporal induction by incremental SAT solving, Electron. Notes Theor. Comput. Sci., 89, 4, 543-560 (2003) · Zbl 1271.68215
[42] González, S. M.; Meseguer, P., Boosting MUS extraction, (Miguel, I.; Ruml, W., SARA (2007)), 285-299
[43] Grégoire, É.; Mazure, B.; Piette MUST, C., Provide a finer-grained explanation of unsatisfiability, (Bessiere, C., CP (2007)), 317-331 · Zbl 1145.68516
[44] Ausiello, G.; D’Atri, A.; Saccà, D., Minimal representation of directed hypergraphs, SIAM J. Comput., 15, 2, 418-431 (1986) · Zbl 0602.68056
[45] Hammer, P. L.; Kogan, A., Optimal compression of propositional horn knowledge bases: complexity and approximation, Artif. Intell., 64, 1, 131-145 (1993) · Zbl 0935.68105
[46] Liberatore, P., Redundancy in logic II: 2CNF and Horn propositional formulae, Artif. Intell., 172, 2-3, 265-299 (2008) · Zbl 1182.68282
[47] Liberatore, P., Redundancy in logic III: non-monotonic reasoning, Artif. Intell., 172, 11, 1317-1359 (2008) · Zbl 1183.68598
[48] Fourdrinoy, O.; Grégoire, É.; Mazure, B.; Saïs, L., Eliminating redundant clauses in SAT instances, (CPAIOR (2007)), 71-83 · Zbl 1214.68333
[49] Piette, C., Let the solver deal with redundancy, (ICTAI (2008)), 67-73
[50] Järvisalo, M.; Heule, M. J.H.; Biere, A., Inprocessing rules, (Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR’12 (2012), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 355-370 · Zbl 1358.68256
[51] Hachtel, G. D.; Somenzi, F., Logic Synthesis and Verification Algorithms (2006), Springer · Zbl 1149.94016
[52] Brayton, R.; Hachtel, G.; McMullen, C.; Sangiovanni-Vincentelli, A., Logic Minimization Algorithms for VLSI Minimization (1985)
[53] Quine, W. V., The problem of simplifying truth functions, Am. Math. Mon., 521-531 (1952) · Zbl 0048.24503
[54] Quine, W. V., A way to simplify truth functions, Am. Math. Mon., 627-631 (1955) · Zbl 0068.24209
[55] McCluskey, E. J., Minimization of Boolean functions, Bell Syst. Tech. J., 35, 6, 1417-1444 (1956)
[56] Coudert, O., Two-level logic minimization: an overview, Integration, 17, 2, 97-140 (1994) · Zbl 0818.94025
[57] Buchfuhrer, D.; Umans, C., The complexity of Boolean formula minimization, J. Comput. Syst. Sci., 77, 1, 142-153 (2011) · Zbl 1218.68089
[58] Umans, C.; Villa, T.; Sangiovanni-Vincentelli, A. L., Complexity of two-level logic minimization, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 25, 7, 1230-1246 (2006)
[59] Chang, C.-W. J.; Marek-Sadowska, M., Theory of wire addition and removal in combinational boolean networks, Microelectron. Eng., 84, 2, 229-243 (2007)
[60] Chen, Y.-C.; Wang, C.-Y., Logic restructuring using node addition and removal, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 31, 2, 260-270 (2012)
[61] Kaiser, A.; Küchlin, W., Detecting inadmissible and necessary variables in large propositional formulae, (Intl. Joint Conf. on Automated Reasoning (Short Papers) (2001), University of Siena), 96-102
[62] Janota, M., Do SAT solvers make good configurators?, (Workshop on Analyses of Software Product Lines (ASPL) (2008)), 191-195
[63] Janota, M., SAT solving in interactive configuration (Nov. 2010), University College Dublin, Ph.D. thesis
[64] Codish, M.; Fekete, Y.; Metodi, A., Backbones for equality, (Bertacco, V.; Legay, A., Haifa Verification Conference (2013), Springer), 1-14
[65] van Maaren, H.; Wieringa, S., Finding guaranteed MUSes fast, (SAT (2008)), 291-304 · Zbl 1138.68555
[67] Piette, C.; Hamadi, Y.; Saïs, L., Efficient combination of decision procedures for MUS computation, (FroCos (2009)), 335-349 · Zbl 1193.68226
[68] Monasson, R.; Zecchina, R.; Kirkpatrick, S.; Selman, B.; Troyansk, L., Determining computational complexity from characteristic ‘phase transitions’, Nature, 400, 133-137 (1999) · Zbl 1369.68244
[69] Bollobás, B.; Borgs, C.; Chayes, J. T.; Kim, J. H.; Wilson, D. B., The scaling window of the 2-SAT transition, Random Struct. Algorithms, 18, 3, 201-256 (2001) · Zbl 0979.68053
[70] Kilby, P.; Slaney, J. K.; Thiébaux, S.; Walsh, T., Backbones and backdoors in satisfiability, (AAAI Conference on Artificial Intelligence (2005)), 1368-1373
[71] Janota, M.; Lynce, I.; Marques-Silva, J., Algorithms for computing backbones of propositional formulae, AI-Com RCRA 2012 special issue, available at
[72] Marques-Silva, J.; Heras, F.; Janota, M.; Previti, A.; Belov, A., On computing minimal correction subsets, (Rossi, F., IJCAI’13 (2013), AAAI Press), 615-622
[74] (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press) · Zbl 1183.68568
[75] (Milano, M., Principles and Practice of Constraint Programming — 18th International Conference, CP 2012, Proceedings. Principles and Practice of Constraint Programming — 18th International Conference, CP 2012, Proceedings, Québec City, QC, Canada, October 8-12, 2012 (2012), Springer) · Zbl 1251.68026
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.