Definability for model counting. (English) Zbl 1435.68304
Summary: We define and evaluate a new preprocessing technique for propositional model counting. This technique leverages definability, i.e., the ability to determine that some gates are implied by the input formula \(\Sigma \). Such gates can be exploited to simplify \(\Sigma\) without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition \(\langle I, O \rangle\) of the variables of \(\Sigma\) where the variables from \(O\) are defined in \(\Sigma\) in terms of \(I\), then eliminating some variables of \(O\) in \(\Sigma \). Our experiments show the computational benefits which can be achieved by taking advantage of our preprocessing technique for model counting.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 03B05 | Classical propositional logic |
| 68R07 | Computational aspects of satisfiability |
| 94C11 | Switching theory, applications of Boolean algebras to circuits and networks |
References:
| [1] | Sang, T.; Beame, P.; Kautz, H. A., Performing Bayesian inference by weighted model counting, (Veloso, M. M.; Kambhampati, S., Proceedings, the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference. Proceedings, the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, Pittsburgh, Pennsylvania, USA, July 9-13, 2005 (2005), AAAI Press/The MIT Press), 475-482 |
| [2] | Chavira, M.; Darwiche, A., On probabilistic inference by weighted model counting, Artif. Intell., 172, 6-7, 772-799 (2008) · Zbl 1182.68297 |
| [3] | Apsel, U.; Brafman, R. I., Lifted MEU by weighted model counting, (Hoffmann, J.; Selman, B., Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, Toronto, Ontario, Canada, July 22-26, 2012 (2012), AAAI Press), 1861-1867 |
| [4] | Choi, A.; Kisa, D.; Darwiche, A., Compiling probabilistic graphical models using sentential decision diagrams, (van der Gaag, L. C., Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 12th European Conference. Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 12th European Conference, ECSQARU 2013, Utrecht, The Netherlands, July 8-10, 2013. Proceedings. Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 12th European Conference. Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 12th European Conference, ECSQARU 2013, Utrecht, The Netherlands, July 8-10, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7958 (2013), Springer), 121-132 · Zbl 1390.68640 |
| [5] | Palacios, H.; Bonet, B.; Darwiche, A.; Geffner, H., Pruning conformant plans by counting models on compiled d-DNNF representations, (Biundo, S.; Myers, K. L.; Rajan, K., Proceedings of the Fifteenth International Conference on Automated Planning and Scheduling. Proceedings of the Fifteenth International Conference on Automated Planning and Scheduling, ICAPS 2005, June 5-10 2005, Monterey, California, USA (2005), AAAI), 141-150 |
| [6] | Domshlak, C.; Hoffmann, J., Fast probabilistic planning through weighted model counting, (Long, D.; Smith, S. F.; Borrajo, D.; McCluskey, L., Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling. Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling, ICAPS 2006, Cumbria, UK, June 6-10, 2006 (2006), AAAI), 243-252 |
| [7] | Feiten, L.; Sauer, M.; Schubert, T.; Czutro, A.; Böhl, E.; Polian, I.; Becker, B., #SAT-based vulnerability analysis of security components – a case study, (2012 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems. 2012 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, DFT 2012, Austin, TX, USA, October 3-5, 2012 (2012), IEEE Computer Society) |
| [8] | Chakraborty, S.; Fried, D.; Meel, K. S.; Vardi, M. Y., From weighted to unweighted model counting, (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), 689-695 |
| [9] | Valiant, L. G., The complexity of computing the permanent, Theor. Comput. Sci., 8, 189-201 (1979) · Zbl 0415.68008 |
| [10] | Roth, D., On the hardness of approximate reasoning, Artif. Intell., 82, 1-2, 273-302 (1996) · Zbl 1506.68143 |
| [11] | Dyer, M. E.; Goldberg, L. A.; Jerrum, M., The complexity of weighted Boolean #CSP, SIAM J. Comput., 38, 5, 1970-1986 (2009) · Zbl 1191.68351 |
| [12] | Toda, S., PP is as hard as the polynomial-time hierarchy, SIAM J. Comput., 20, 5, 865-877 (1991) · Zbl 0733.68034 |
| [13] | Samer, M.; Szeider, S., Algorithms for propositional model counting, J. Discret. Algorithms, 8, 1, 50-64 (2010) · Zbl 1214.05166 |
| [14] | Bacchus, F.; Dalmao, S.; Pitassi, T., Algorithms and complexity results for #SAT and Bayesian inference, (44th Symposium on Foundations of Computer Science. 44th Symposium on Foundations of Computer Science, FOCS 2003, 11-14 October 2003, Cambridge, MA, USA, Proceedings (2003), IEEE Computer Society), 340-351 |
| [15] | Gomes, C. P.; Sabharwal, A.; Selman, B., Model counting, (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), 633-654 · Zbl 1183.68568 |
| [16] | Achlioptas, D.; Hammoudeh, Z.; Theodoropoulos, P., Fast and flexible probabilistic model counting, in: Beyersdorff and Wintersteiger [80], pp. 148-164 · Zbl 1511.68242 |
| [17] | Achlioptas, D.; Theodoropoulos, P., Probabilistic model counting with short XORs, (Gaspers, S.; Walsh, T., Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference. Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference. Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10491 (2017), Springer), 3-19 · Zbl 1496.68253 |
| [18] | S. Chakraborty, K.S. Meel, M.Y. Vardi, Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls, in: Kambhampati [81], pp. 3569-3576. |
| [19] | Bacchus, F.; Winter, J., Effective preprocessing with hyper-resolution and equality reduction, (Giunchiglia, E.; Tacchella, A., Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919 (2003), Springer), 341-355 · Zbl 1204.68176 |
| [20] | S. Subbarayan, D.K. Pradhan Niver, Non increasing variable elimination resolution for preprocessing SAT instances, in: SAT 2004 - the Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, in: Online Proceedings [82], Vancouver, BC, Canada, pp. 276-291. · Zbl 1122.68618 |
| [21] | Lynce, I.; Marques Silva, J. P., Probing-based preprocessing techniques for propositional satisfiability, (15th IEEE International Conference on Tools with Artificial Intelligence. 15th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2003, 3-5 November 2003, Sacramento, California, USA (2003), IEEE Computer Society), 105 |
| [22] | Eén, N.; Biere, A., Effective preprocessing in SAT through variable and clause elimination, (Bacchus, F.; Walsh, T., Theory and Applications of Satisfiability Testing, 8th International Conference. Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings. Theory and Applications of Satisfiability Testing, 8th International Conference. Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3569 (2005), Springer), 61-75 · Zbl 1128.68463 |
| [23] | Piette, C.; Hamadi, Y.; Sais, L., Vivifying propositional clausal formulae, (Ghallab, M.; Spyropoulos, C. D.; Fakotakis, N.; Avouris, N. M., ECAI 2008 - 18th European Conference on Artificial Intelligence. ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings. ECAI 2008 - 18th European Conference on Artificial Intelligence. ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings, Frontiers in Artificial Intelligence and Applications, vol. 178 (2008), IOS Press), 525-529 |
| [24] | Han, H.; Somenzi, F., Alembic: an efficient algorithm for CNF preprocessing, (Proceedings of the 44th Design Automation Conference. Proceedings of the 44th Design Automation Conference, DAC 2007, San Diego, CA, USA, June 4-8, 2007 (2007), IEEE), 582-587 |
| [25] | Heule, M.; Järvisalo, M.; Biere, A., Clause elimination procedures for CNF formulas, (Fermüller, C. G.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6397 (2010), Springer), 357-371 · Zbl 1306.68144 |
| [26] | Järvisalo, M.; Biere, A.; Heule, M., Simulating circuit-level simplifications on CNF, J. Autom. Reason., 49, 4, 583-619 (2012) · Zbl 1267.94144 |
| [27] | Heule, M.; Järvisalo, M.; Biere, A., Efficient CNF simplification based on binary implication graphs, (Sakallah, K. A.; Simon, L., Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference. Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference. Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6695 (2011), Springer), 201-215 · Zbl 1330.68269 |
| [28] | Audemard, G.; Simon, L., Predicting learnt clauses quality in modern SAT solvers, (Boutilier, C., IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence. IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009 (2009)), 399-404 |
| [29] | Biere, A., Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver lingeling, (Le Berre, D., POS-14. Fifth Pragmatics of SAT Workshop, a Workshop of the SAT 2014 Conference, part of FLoC 2014 During the Vienna Summer of Logic. POS-14. Fifth Pragmatics of SAT Workshop, a Workshop of the SAT 2014 Conference, part of FLoC 2014 During the Vienna Summer of Logic, July 13, 2014, Vienna, Austria. POS-14. Fifth Pragmatics of SAT Workshop, a Workshop of the SAT 2014 Conference, part of FLoC 2014 During the Vienna Summer of Logic. POS-14. Fifth Pragmatics of SAT Workshop, a Workshop of the SAT 2014 Conference, part of FLoC 2014 During the Vienna Summer of Logic, July 13, 2014, Vienna, Austria, EPiC Series in Computing, vol. 27 (2014), EasyChair), 88 |
| [30] | Manthey, N., Solver Description of RISS 2.0 and PRISS 2.0 (2012), TU Dresden, Knowledge Representation and Reasoning, Tech. rep. |
| [31] | Manthey, N., Coprocessor 2.0 - A flexible CNF simplifier - (tool presentation), in: Cimatti and Sebastiani [83], pp. 436-441 |
| [32] | Lagniez, J.-M.; Marquis, P., On preprocessing techniques and their impact on propositional model counting, J. Autom. Reason., 58, 4, 413-481 (2017) · Zbl 1409.68259 |
| [33] | Lang, J.; Marquis, P., On propositional definability, Artif. Intell., 172, 8-9, 991-1017 (2008) · Zbl 1183.68607 |
| [34] | Tseitin, G., On the complexity of derivation in propositional calculus, (Structures in Constructive Mathematics and Mathematical Logic (1968), Steklov Mathematical Institute), 115-125 · Zbl 0197.00102 |
| [35] | Plaisted, D. A.; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304 (1986) · Zbl 0636.68119 |
| [36] | J.-M. Lagniez, E. Lonca, P. Marquis, Improving model counting by leveraging definability, in: Kambhampati [81], pp. 751-757. |
| [37] | Lagniez, J.-M.; Marquis, P., An improved decision-DNNF compiler, (Sierra, C., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 (2017)), 667-673 |
| [38] | Gebser, M.; Kaufmann, B.; Schaub, T., Solution enumeration for projected Boolean search problems, (van Hoeve, W. J.; Hooker, J. N., Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 6th International Conference. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 6th International Conference, CPAIOR 2009, Pittsburgh, PA, USA, May 27-31, 2009, Proceedings. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 6th International Conference. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 6th International Conference, CPAIOR 2009, Pittsburgh, PA, USA, May 27-31, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5547 (2009), Springer), 71-86 · Zbl 1241.68100 |
| [39] | Aziz, R. A.; Chu, G.; Muise, C. J.; Stuckey, P. J., #∃SAT: projected model counting, (Heule, M.; Weaver, S., Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9340 (2015), Springer), 121-137 · Zbl 1471.68174 |
| [40] | 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 |
| [41] | Enderton, H. B., A Mathematical Introduction to Logic (1972), Academic Press · Zbl 0298.02002 |
| [42] | Lang, J.; Liberatore, P.; Marquis, P., Propositional independence: formula-variable independence and forgetting, J. Artif. Intell. Res., 18, 391-443 (2003) · Zbl 1056.68112 |
| [43] | Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203 |
| [44] | Beth, E., On Padoa’s method in the theory of definition, Indag. Math., 15, 330-339 (1953) · Zbl 0053.34402 |
| [45] | Padoa, A., Essai d’une théorie algébrique des nombres entiers, précédé d’une introduction logique à une théorie déductive quelconque, (Bibliothèque du Congrès International de Philosophie. Bibliothèque du Congrès International de Philosophie, Paris (1903)), 309-365 |
| [46] | Cook, S. A., The complexity of theorem-proving procedures, (Harrison, M. A.; Banerji, R. B.; Ullman, J. D., Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA (1971), ACM), 151-158 · Zbl 0253.68020 |
| [47] | Marques Silva, J. P.; Sakallah, K. A., GRASP - a new search algorithm for satisfiability, (ICCAD (1996)), 220-227 |
| [48] | Marques Silva, J. P.; Sakallah, K. A., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388 |
| [49] | Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (Proceedings of the 38th Design Automation Conference. Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001 (2001), ACM), 530-535 |
| [50] | Zhang, H.; Stickel, M. E., An efficient algorithm for unit propagation, (Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics. Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics, AI-MATH’96, Fort Lauderdale, Florida USA (1996)), 166-169 |
| [51] | Roussel, O., Controlling a solver execution with the runsolver tool, J. Satisf. Boolean Model. Comput., 7, 4, 139-144 (2011) · Zbl 1331.68210 |
| [52] | Audemard, G.; Lagniez, J.-M.; Simon, L., Improving glucose for incremental SAT solving with assumptions: application to MUS extraction, in: Järvisalo and Gelder [84], pp. 309-317 · Zbl 1390.68587 |
| [53] | T. Sang, F. Bacchus, P. Beame, H.A. Kautz, T. Pitassi, Combining component caching and clause learning for effective model counting, in: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, in: Online Proceedings [82], Vancouver, BC, Canada, pp. 20-28. |
| [54] | Thurley, M., sharpSAT - counting models with advanced component caching and implicit BCP, (Biere, A.; Gomes, C. P., Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference. Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference. Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4121 (2006), Springer), 424-429 |
| [55] | Darwiche, A., Decomposable negation normal form, J. ACM, 48, 4, 608-647 (2001) · Zbl 1127.03321 |
| [56] | Darwiche, A., New advances in compiling CNF into decomposable negation normal form, (de Mántaras, R. L.; Saitta, L., Proceedings of the 16th European Conference on Artificial Intelligence, ECAI’2004, Including Prestigious Applicants of Intelligent Systems. Proceedings of the 16th European Conference on Artificial Intelligence, ECAI’2004, Including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004 (2004), IOS Press), 328-332 |
| [57] | Samer, M.; Szeider, S., Algorithms for propositional model counting, J. Discret. Algorithms, 8, 1, 50-64 (2010) · Zbl 1214.05166 |
| [58] | Cadoli, M.; Donini, F. M.; Schaerf, M.; Silvestri, R., On compact representations of propositional circumscription, Theor. Comput. Sci., 182, 1-2, 183-202 (1997) · Zbl 0901.68189 |
| [59] | del Val, A., An analysis of approximate knowledge compilation, (Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, 2 Volumes (1995), Morgan Kaufmann), 830-836 |
| [60] | Bart, A.; Koriche, F.; Lagniez, J.-M.; Marquis, P., Symmetry-driven decision diagrams for knowledge compilation, (Schaub, T.; Friedrich, G.; O’Sullivan, B., 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, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), Frontiers in Artificial Intelligence and Applications, vol. 263 (2014), IOS Press), 51-56 · Zbl 1366.68300 |
| [61] | Fichte, J. K.; Hecher, M.; Morak, M.; Woltran, S., Exploiting treewidth for projected model counting and its limits, in: Beyersdorff and Wintersteiger [80], pp. 165-184 · Zbl 1511.68195 |
| [62] | Durand, A.; Hermann, M.; Kolaitis, P. G., Subtractive reductions and complete problems for counting complexity classes, Theor. Comput. Sci., 340, 3, 496-513 (2005) · Zbl 1077.68033 |
| [63] | Klebanov, V.; Manthey, N.; Muise, C. J., SAT-based analysis and quantification of information flow in programs, (Joshi, K. R.; Siegle, M.; Stoelinga, M.; D’Argenio, P. R., Quantitative Evaluation of Systems - 10th International Conference. Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Quantitative Evaluation of Systems - 10th International Conference. Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8054 (2013), Springer), 177-192 |
| [64] | Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, J. Symb. Log., 22, 269-285 (1957) · Zbl 0079.24502 |
| [65] | Brauer, J.; King, A.; Kriener, J., Existential quantification as incremental SAT, (Gopalakrishnan, G.; Qadeer, S., Computer Aided Verification - 23rd International Conference. Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Computer Aided Verification - 23rd International Conference. Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806 (2011), Springer), 191-207 |
| [66] | Zengler, C.; Küchlin, W., Boolean quantifier elimination for automotive configuration - a case study, (Pecheur, C.; Dierkes, M., Formal Methods for Industrial Critical Systems - 18th International Workshop. Formal Methods for Industrial Critical Systems - 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013, Proceedings. Formal Methods for Industrial Critical Systems - 18th International Workshop. Formal Methods for Industrial Critical Systems - 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013, Proceedings, Lecture Notes in Computer Science, vol. 8187 (2013), Springer), 48-62 |
| [67] | Brauer, J.; King, A., Approximate quantifier elimination for propositional Boolean formulae, (Bobaru, M. G.; Havelund, K.; Holzmann, G. J.; Joshi, R., NASA Formal Methods - Third International Symposium. NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. NASA Formal Methods - Third International Symposium. NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6617 (2011), Springer), 73-88 |
| [68] | Monniaux, D., Quantifier elimination by lazy model enumeration, (Touili, T.; Cook, B.; Jackson, P. B., Computer Aided Verification, 22nd International Conference. Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings. Computer Aided Verification, 22nd International Conference. Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6174 (2010), Springer), 585-599 |
| [69] | Schrag, R., Compilation for critically constrained knowledge bases, (Clancey, W. J.; Weld, D. S., Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference. Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, AAAI 96, IAAI 96, Portland, Oregon, USA, August 4-8, 1996, Volume 1 (1996), AAAI Press/The MIT Press), 510-515 |
| [70] | Gupta, A.; Yang, Z.; Ashar, P.; Gupta, A., SAT-based image computation with application in reachability analysis, (Jr., W. A.H.; Johnson, S. D., Formal Methods in Computer-Aided Design, Third International Conference. Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings. Formal Methods in Computer-Aided Design, Third International Conference. Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1954 (2000), Springer), 354-371 |
| [71] | Darwiche, A.; Marquis, P., A knowledge compilation map, J. Artif. Intell. Res., 17, 229-264 (2002) · Zbl 1045.68131 |
| [72] | Nadel, A., Boosting minimal unsatisfiable core extraction, (Bloem, R.; Sharygina, N., Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010. Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, FMCAD 2010, Lugano, Switzerland, October 20-23 (2010), IEEE), 221-229 |
| [73] | Belov, A.; Marques Silva, J. P., Muser2: an efficient MUS extractor, J. Satisf. Boolean Model. Comput., 8, 3/4, 123-128 (2012) · Zbl 1322.68178 |
| [74] | Janota, M.; Marques Silva, J. P., On deciding MUS membership with QBF, (Lee, J. H., Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference. Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011, Proceedings. Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference. Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6876 (2011), Springer), 414-428 |
| [75] | Belov, A.; Ivrii, A.; Matsliah, A.; Marques Silva, J. P., On efficient computation of variable MUSes, in: Cimatti and Sebastiani [83], pp. 298-311 · Zbl 1273.03047 |
| [76] | Lagniez, J.-M.; Biere, A., Factoring out assumptions to speed up MUS extraction, in: Järvisalo and Gelder [84], pp. 276-292 · Zbl 1390.68601 |
| [77] | Marques Silva, J. P.; Previti, A., On computing preferred MUSes and MCSes, (Sinz, C.; Egly, U., Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8561 (2014), Springer), 58-74 · Zbl 1423.68460 |
| [78] | Ignatiev, A.; Previti, A.; Liffiton, M. H.; Marques Silva, J. P., Smallest MUS extraction with minimal hitting set dualization, (Pesant, G., Principles and Practice of Constraint Programming - 21st International Conference. Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings. Principles and Practice of Constraint Programming - 21st International Conference. Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9255 (2015), Springer), 173-182 · Zbl 1318.68035 |
| [79] | Kullmann, O., On a generalization of extended resolution, Discrete Appl. Math., 96-97, 149-176 (1999) · Zbl 0941.68126 |
| [80] | (Beyersdorff, O.; Wintersteiger, C. M., Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference. Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference. Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10929 (2018), Springer) · Zbl 1390.68015 |
| [81] | (Kambhampati, S., Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016 (2016), IJCAI/AAAI Press) |
| [82] | SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Online Proceedings, Vancouver, BC, Canada. |
| [83] | (Cimatti, A.; Sebastiani, R., Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference. Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference. Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317 (2012), Springer) · Zbl 1268.68009 |
| [84] | (Järvisalo, M.; Gelder, A. V., Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference. Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference. Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7962 (2013), Springer) · Zbl 1268.68023 |
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.
