{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:14:23Z","timestamp":1761549263006,"version":"build-2065373602"},"reference-count":39,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2024,11,5]],"date-time":"2024-11-05T00:00:00Z","timestamp":1730764800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SAT"],"abstract":"<jats:p>Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT\u201922). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MIC E \u2032 that is polynomially equivalent to MICE. We then establish an exponential lower bound for the number of proof steps in MIC E \u2032 (and hence also in MICE) for a specific family of CNFs. We also explain a tight connection between MIC E \u2032 proofs and decision DNNFs.<\/jats:p>","DOI":"10.3233\/sat-231507","type":"journal-article","created":{"date-parts":[[2024,11,5]],"date-time":"2024-11-05T12:30:43Z","timestamp":1730809843000},"page":"27-59","source":"Crossref","is-referenced-by-count":0,"title":["Proof Complexity of Propositional Model Counting"],"prefix":"10.1177","volume":"15","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Friedrich Schiller University Jena, Germany"}]},{"given":"Tim","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Friedrich Schiller University Jena, Germany"}]},{"given":"Luc N.","family":"Spachmann","sequence":"additional","affiliation":[{"name":"Friedrich Schiller University Jena, Germany"}]}],"member":"179","published-online":{"date-parts":[[2024,11,5]]},"reference":[{"key":"10.3233\/SAT-231507_ref1","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1613\/jair.3152","article-title":"Clause-learning algorithms with many restarts and bounded-width resolution","volume":"40","author":"Atserias","year":"2011","journal-title":"J. Artif. Intell. Res."},{"key":"10.3233\/SAT-231507_ref2","doi-asserted-by":"crossref","unstructured":"F.\u00a0Bacchus, S.\u00a0Dalmao and T.\u00a0Pitassi, Algorithms and complexity results for #SAT and Bayesian inference, in: 44th Symposium on Foundations of Computer Science (FOCS 2003), Proceedings, Cambridge, MA, USA, 11\u201314 October 2003, IEEE Computer Society, 2003, pp.\u00a0340\u2013351.","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"10.3233\/SAT-231507_ref3","doi-asserted-by":"crossref","unstructured":"T.\u00a0Baluta, Z.L.\u00a0Chua, K.S.\u00a0Meel and P.\u00a0Saxena, Scalable quantitative verification for deep neural networks, in: 43rd IEEE\/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22\u201330 May 2021, IEEE, 2021, pp.\u00a0312\u2013323.","DOI":"10.1109\/ICSE43902.2021.00039"},{"key":"10.3233\/SAT-231507_ref4","unstructured":"P.\u00a0Beame, J.\u00a0Li, S.\u00a0Roy and D.\u00a0Suciu, Lower bounds for exact model counting and applications in probabilistic databases, in: Proceedings of the Twenty-Ninth Conference on Uncertainty in Artificial Intelligence, UAI 2013, Bellevue, WA, USA, August 11\u201315, 2013, A.E.\u00a0Nicholson and P.\u00a0Smyth, eds, AUAI Press, 2013."},{"key":"10.3233\/SAT-231507_ref5","unstructured":"P.\u00a0Beame, J.\u00a0Li, S.\u00a0Roy and D.\u00a0Suciu, Lower bounds for exact model counting and applications in probabilistic databases, in: Proceedings of the Twenty-Ninth Conference on Uncertainty in Artificial Intelligence, UAI 2013, Bellevue, WA, USA, August 11\u201315, 2013, A.E.\u00a0Nicholson and P.\u00a0Smyth, eds, AUAI Press, 2013."},{"key":"10.3233\/SAT-231507_ref6","unstructured":"O.\u00a0Beyersdorff and B.\u00a0B\u00f6hm, Understanding the relative strength of QBF CDCL solvers and QBF resolution, in: 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a0185, 2021, pp.\u00a012:1\u201312:20."},{"key":"10.3233\/SAT-231507_ref7","unstructured":"O.\u00a0Beyersdorff, T.\u00a0Hoffmann and L.N.\u00a0Spachmann, Proof complexity of propositional model counting, in: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT), M.\u00a0Mahajan and F.\u00a0Slivovsky, eds, LIPIcs, Vol.\u00a0271, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2023, pp.\u00a02:1\u20132:18."},{"key":"10.3233\/SAT-231507_ref8","doi-asserted-by":"crossref","unstructured":"A.\u00a0Biere, M.\u00a0Heule, H.\u00a0van Maaren and T.\u00a0Walsh\u00a0(eds), Handbook of Satisfiability, in Frontiers in Artificial Intelligence and Applications, IOS Press, 2021.","DOI":"10.3233\/FAIA336"},{"key":"10.3233\/SAT-231507_ref9","doi-asserted-by":"crossref","unstructured":"B.\u00a0B\u00f6hm and O.\u00a0Beyersdorff, Lower bounds for QCDCL via formula gauge, in: Theory and Applications of Satisfiability Testing (SAT), C.-M.\u00a0Li and F.\u00a0Many\u00e0, eds, Springer International Publishing, Cham, 2021, pp.\u00a047\u201363.","DOI":"10.1007\/978-3-030-80223-3_5"},{"key":"10.3233\/SAT-231507_ref10","doi-asserted-by":"crossref","unstructured":"B.\u00a0B\u00f6hm, T.\u00a0Peitl and O.\u00a0Beyersdorff, QCDCL with cube learning or pure literal elimination \u2013 what is best? in: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI), L.D.\u00a0Raedt, ed., ijcai.org, 2022, pp.\u00a01781\u20131787.","DOI":"10.24963\/ijcai.2022\/248"},{"key":"10.3233\/SAT-231507_ref12","unstructured":"S.\u00a0Bova, F.\u00a0Capelli, S.\u00a0Mengel and F.\u00a0Slivovsky, Knowledge compilation meets communication complexity, in: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI), S.\u00a0Kambhampati, ed., IJCAI\/AAAI Press, 2016, pp.\u00a01008\u20131014."},{"key":"10.3233\/SAT-231507_ref13","unstructured":"R.E.\u00a0Bryant, W.\u00a0Nawrocki, J.\u00a0Avigad and M.J.H.\u00a0Heule, Certified knowledge compilation with application to verified model counting, in: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT), M.\u00a0Mahajan and F.\u00a0Slivovsky, eds, LIPIcs, Vol.\u00a0271, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2023, pp.\u00a06:1\u20136:20."},{"key":"10.3233\/SAT-231507_ref14","doi-asserted-by":"crossref","unstructured":"S.\u00a0Buss and J.\u00a0Nordstr\u00f6m, Proof complexity and SAT solving, in: Handbook of Satisfiability, A.\u00a0Biere, M.\u00a0Heule, H.\u00a0van Maaren and T.\u00a0Walsh, eds, Frontiers in Artificial Intelligence and Applications, IOS Press, 2021, pp.\u00a0233\u2013350.","DOI":"10.3233\/FAIA200990"},{"key":"10.3233\/SAT-231507_ref15","doi-asserted-by":"crossref","unstructured":"S.\u00a0Buss and N.\u00a0Thapen, DRAT proofs, propagation redundancy, and extended resolution, in: Theory and Applications of Satisfiability Testing (SAT), M.\u00a0Janota and I.\u00a0Lynce, eds, Lecture Notes in Computer Science, Vol.\u00a011628, Springer, 2019, pp.\u00a071\u201389.","DOI":"10.1007\/978-3-030-24258-9_5"},{"key":"10.3233\/SAT-231507_ref16","doi-asserted-by":"crossref","unstructured":"F.\u00a0Capelli, Knowledge compilation languages as proof systems, in: Theory and Applications of Satisfiability Testing (SAT), M.\u00a0Janota and I.\u00a0Lynce, eds, Lecture Notes in Computer Science, Vol.\u00a011628, Springer, 2019, pp.\u00a090\u201399.","DOI":"10.1007\/978-3-030-24258-9_6"},{"key":"10.3233\/SAT-231507_ref17","doi-asserted-by":"crossref","unstructured":"F.\u00a0Capelli, J.\u00a0Lagniez and P.\u00a0Marquis, Certifying top-down decision-DNNF compilers, in: Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI) 2021, AAAI Press, 2021, pp.\u00a06244\u20136253.","DOI":"10.1609\/aaai.v35i7.16776"},{"key":"10.3233\/SAT-231507_ref18","unstructured":"L.\u00a0Chew and M.J.H.\u00a0Heule, Relating existing powerful proof systems for QBF, in: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), K.S.\u00a0Meel and O.\u00a0Strichman, eds, LIPIcs, Vol.\u00a0236, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2022, pp.\u00a010:1\u201310:22."},{"key":"10.3233\/SAT-231507_ref19","doi-asserted-by":"crossref","unstructured":"S.A.\u00a0Cook, The complexity of theorem proving procedures, in: Proc. 3rd Annual ACM Symposium on Theory of Computing, 1971, pp.\u00a0151\u2013158.","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"10.3233\/SAT-231507_ref20","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"J. Symb. Log."},{"issue":"4","key":"10.3233\/SAT-231507_ref21","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","article-title":"Decomposable negation normal form","volume":"48","author":"Darwiche","year":"2001","journal-title":"J. ACM"},{"key":"10.3233\/SAT-231507_ref22","unstructured":"L.\u00a0Due\u00f1as-Osorio, K.S.\u00a0Meel, R.\u00a0Paredes and M.Y.\u00a0Vardi, Counting-based reliability estimation for power-transmission grids, in: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, San Francisco, California, USA, February 4-9, 2017, S.\u00a0Singh and S.\u00a0Markovitch, eds, AAAI Press, 2017, pp.\u00a04488\u20134494."},{"key":"10.3233\/SAT-231507_ref23","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/3459080","article-title":"The model counting competition 2020","volume":"26","author":"Fichte","year":"2021","journal-title":"ACM J. Exp. Algorithmics"},{"key":"10.3233\/SAT-231507_ref24","unstructured":"J.K.\u00a0Fichte, M.\u00a0Hecher and V.\u00a0Roland, Proofs for propositional model counting, in: 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, August 2\u20135, 2022, K.S.\u00a0Meel and O.\u00a0Strichman, eds, LIPIcs, Vol.\u00a0236, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2022, pp.\u00a030:1\u201330:24."},{"key":"10.3233\/SAT-231507_ref25","doi-asserted-by":"crossref","unstructured":"J.K.\u00a0Fichte, M.\u00a0Hecher, P.\u00a0Thier and S.\u00a0Woltran, Exploiting database management systems and treewidth for counting, in: Practical Aspects of Declarative Languages \u2013 22nd International Symposium, PADL 2020, Proceedings, New Orleans, LA, USA, January 20\u201321, 2020, E.\u00a0Komendantskaya and Y.A.\u00a0Liu, eds, Lecture Notes in Computer Science, Vol.\u00a012007, Springer, 2020, pp.\u00a0151\u2013167.","DOI":"10.1007\/978-3-030-39197-3_10"},{"key":"10.3233\/SAT-231507_ref26","unstructured":"C.P.\u00a0Gomes, A.\u00a0Sabharwal and B.\u00a0Selman, Model counting, in: Handbook of Satisfiability, A.\u00a0Biere, M.\u00a0Heule, H.\u00a0van Maaren and T.\u00a0Walsh, eds, Frontiers in Artificial Intelligence and Applications, Vol.\u00a0336, 2nd edn, IOS Press, 2021, pp.\u00a0993\u20131014."},{"key":"10.3233\/SAT-231507_ref27","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theor. Comput. Sci."},{"key":"10.3233\/SAT-231507_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_24"},{"issue":"1","key":"10.3233\/SAT-231507_ref29","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-016-9390-4","article-title":"Solution validation and extraction for QBF preprocessing","volume":"58","author":"Heule","year":"2017","journal-title":"J. Autom. Reason."},{"key":"10.3233\/SAT-231507_ref30","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lagniez and P.\u00a0Marquis, An improved decision-DNNF compiler, in: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19\u201325, 2017, C.\u00a0Sierra, ed., ijcai.org, 2017, pp.\u00a0667\u2013673.","DOI":"10.24963\/ijcai.2017\/93"},{"key":"10.3233\/SAT-231507_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_32"},{"key":"10.3233\/SAT-231507_ref32","doi-asserted-by":"crossref","unstructured":"J.P.\u00a0Marques Silva, I.\u00a0Lynce and S.\u00a0Malik, Conflict-driven clause learning SAT solvers, in: Handbook of Satisfiability, A.\u00a0Biere, M.\u00a0Heule, H.\u00a0van Maaren and T.\u00a0Walsh, eds, Frontiers in Artificial Intelligence and Applications, IOS Press, 2021.","DOI":"10.3233\/FAIA200987"},{"issue":"2","key":"10.3233\/SAT-231507_ref33","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","article-title":"On the power of clause-learning SAT solvers as resolution engines","volume":"175","author":"Pipatsrisawat","year":"2011","journal-title":"Artif. Intell."},{"key":"10.3233\/SAT-231507_ref34","doi-asserted-by":"crossref","unstructured":"W.\u00a0Shi, A.\u00a0Shih, A.\u00a0Darwiche and A.\u00a0Choi, On tractable representations of binary neural networks, in: Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12\u201318, 2020, D.\u00a0Calvanese, E.\u00a0Erdem and M.\u00a0Thielscher, eds, 2020, pp.\u00a0882\u2013892.","DOI":"10.24963\/kr.2020\/91"},{"key":"10.3233\/SAT-231507_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_38"},{"issue":"5","key":"10.3233\/SAT-231507_ref36","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1137\/0220053","article-title":"PP is as hard as the polynomial-time hierarchy","volume":"20","author":"Toda","year":"1991","journal-title":"SIAM J. Comput."},{"issue":"3","key":"10.3233\/SAT-231507_ref37","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2578043","article-title":"Boolean satisfiability: Theory and engineering","volume":"57","author":"Vardi","year":"2014","journal-title":"Commun. ACM"},{"key":"10.3233\/SAT-231507_ref38","doi-asserted-by":"crossref","unstructured":"M.\u00a0Vinyals, Hard examples for common variable decision heuristics, in: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2020.","DOI":"10.1609\/aaai.v34i02.5527"},{"key":"10.3233\/SAT-231507_ref39","doi-asserted-by":"crossref","unstructured":"N.\u00a0Wetzler, M.\u00a0Heule and W.A.\u00a0Hunt Jr., DRAT-trim: Efficient checking and trimming using expressive clausal proofs, in: Theory and Applications of Satisfiability Testing (SAT), C.\u00a0Sinz and U.\u00a0Egly, eds, Lecture Notes in Computer Science, Vol.\u00a08561, Springer, 2014, pp.\u00a0422\u2013429.","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"10.3233\/SAT-231507_ref40","unstructured":"E.\u00a0Zhai, A.\u00a0Chen, R.\u00a0Piskac, M.\u00a0Balakrishnan, B.\u00a0Tian, B.\u00a0Song and H.\u00a0Zhang, Check before you change: Preventing correlated failures in service updates, in: 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, February 25\u201327, 2020, R.\u00a0Bhagwan and G.\u00a0Porter, eds, USENIX Association, 2020, pp.\u00a0575\u2013589."}],"container-title":["Journal on Satisfiability, Boolean Modeling and Computation"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/SAT-231507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:08:27Z","timestamp":1761548907000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/SAT-231507"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,5]]},"references-count":39,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,11,5]]}},"URL":"https:\/\/doi.org\/10.3233\/sat-231507","relation":{},"ISSN":["1574-0617"],"issn-type":[{"type":"electronic","value":"1574-0617"}],"subject":[],"published":{"date-parts":[[2024,11,5]]}}}