{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T04:24:52Z","timestamp":1775276692488,"version":"3.50.1"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T00:00:00Z","timestamp":1459987200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["BR4CP ANR-11-BS02-008"],"award-info":[{"award-number":["BR4CP ANR-11-BS02-008"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s10817-016-9370-8","type":"journal-article","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T06:20:49Z","timestamp":1460010049000},"page":"413-481","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["On Preprocessing Techniques and Their Impact on Propositional Model Counting"],"prefix":"10.1007","volume":"58","author":[{"given":"Jean-Marie","family":"Lagniez","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Marquis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,7]]},"reference":[{"issue":"12","key":"9370_CR1","first-page":"1562","volume":"10","author":"FA Aloul","year":"2004","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: MINCE: a static global variable-ordering heuristic for SAT search and BDD manipulation. J. UCS 10(12), 1562\u20131596 (2004)","journal-title":"J. UCS"},{"key":"9370_CR2","unstructured":"Apsel, U., Brafman, R.I.: Lifted MEU by weighted model counting. In: Proceedings of AAAI\u201912 (2012)"},{"key":"9370_CR3","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Just-in-time compilation of knowledge bases. In: Proceedings of IJCAI\u201913, pp. 447\u2013453 (2013)"},{"key":"9370_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solver. In: Proceedings of IJCAI\u201909, pp. 399\u2013404 (2009)"},{"key":"9370_CR5","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Proceedings of SAT\u201904, pp. 341\u2013355 (2004)","DOI":"10.1007\/978-3-540-24605-3_26"},{"key":"9370_CR6","unstructured":"Bayardo, R.J., Jr. Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of AAAI\u201997, pp. 203\u2013208 (1997)"},{"key":"9370_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the the SAT solver lingeling. In: Proceedings of POS\u201914. Fifth Pragmatics of SAT Workshop, a Workshop of the SAT 2014 Conference, Part of FLoC 2014 During the Vienna Summer of Logic, pp.\u00a088 (2014)","DOI":"10.29007\/jhd7"},{"key":"9370_CR8","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"},{"key":"9370_CR9","unstructured":"Bordeaux, L., Janota, M., Marques-Silva, J., Marquis, P.: On unit-refutation complete formulae with existentially quantified variables. In: Proceedings of KR\u201912, pp. 75\u201384 (2012)"},{"key":"9370_CR10","doi-asserted-by":"crossref","unstructured":"Bordeaux L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Proceedings of SOFSEM\u201912, pp. 612\u2013624 (2012)","DOI":"10.1007\/978-3-642-27660-6_50"},{"key":"9370_CR11","unstructured":"Boufkhad, Y., Gr\u00e9goire, E., Marquis, P., Mazure, B., Sa\u00efs, L.: Tractable cover compilations. In: Proceedings of IJCAI\u201997, pp. 122\u2013127 (1997)"},{"key":"9370_CR12","unstructured":"Boufkhad, Y., Roussel, O.: Redundancy in random SAT formulas. In: Proceedings of AAAI\u201900, pp. 273\u2013278 (2000)"},{"key":"9370_CR13","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)"},{"issue":"6\u20137","key":"9370_CR14","doi-asserted-by":"crossref","first-page":"772","DOI":"10.1016\/j.artint.2007.11.002","volume":"172","author":"M Chavira","year":"2008","unstructured":"Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6\u20137), 772\u2013799 (2008)","journal-title":"Artif. Intell."},{"issue":"4","key":"9370_CR15","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608\u2013647 (2001)","journal-title":"J. ACM"},{"key":"9370_CR16","unstructured":"Darwiche, A.: New advances in compiling cnf into decomposable negation normal form. In: Proceedings of ECAI\u201904, pp. 328\u2013332 (2004)"},{"key":"9370_CR17","unstructured":"Darwiche, A.: SDD: A new canonical representation of propositional knowledge bases. In: Proceedings of IJCAI\u201911, pp. 819\u2013826 (2011)"},{"issue":"7","key":"9370_CR18","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. J. ACM 5(7), 394\u2013397 (1962)","journal-title":"J. ACM"},{"issue":"3","key":"9370_CR19","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9370_CR20","doi-asserted-by":"crossref","unstructured":"del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Proceedings of KR\u201994, pp. 551\u2013561 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"key":"9370_CR21","unstructured":"Domshlak, C., Hoffmann, J.: Fast probabilistic planning through weighted model counting. In: Proceedings of ICAPS\u201906, pp. 243\u2013252 (2006)"},{"key":"9370_CR22","doi-asserted-by":"crossref","unstructured":"Een, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Proceedings of SAT\u201905, pp. 61\u201375 (2005)","DOI":"10.1007\/11499107_5"},{"key":"9370_CR23","unstructured":"Fargier, H., Marquis, P.: Extending the knowledge compilation map: Krom, Horn, affine and beyond. In: Proceedings of AAAI\u201908, pp. 442\u2013447, (2008)"},{"key":"9370_CR24","unstructured":"Freemann, J.W.: Improvement to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania (1995)"},{"key":"9370_CR25","unstructured":"Gomes, C.P., Hoffmann, J.: A.\u00a0Sabharwal, and B.\u00a0Selman. From sampling to model counting. In: Proceedings of IJCAI\u201907, pp. 2293\u20132299 (2007)"},{"key":"9370_CR26","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proceedings of DAC\u201907, pp. 582\u2013587 (2007)","DOI":"10.1145\/1278480.1278628"},{"key":"9370_CR27","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Proceedings of LPAR\u201910, pp. 357\u2013371 (2010)","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"9370_CR28","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Proceedings of LPAR\u201910, pp. 41\u201346 (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"9370_CR29","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Efficient cnf simplification based on binary implication graphs. In: Proceedings of SAT\u201911, pp. 201\u2013215 (2011)","DOI":"10.1007\/978-3-642-21581-0_17"},{"key":"9370_CR30","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9370_CR31","unstructured":"Huang, J., Darwiche, A.: Using DPLL for efficient OBDD construction. In: Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10\u201313, 2004, Revised Selected Papers, pp. 157\u2013172 (2004)"},{"issue":"4","key":"9370_CR32","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583\u2013619 (2012)","journal-title":"J. Autom. Reason."},{"key":"9370_CR33","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In Proceedings of IJCAR\u201912, pp. 355\u2013370 (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9370_CR34","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"issue":"2","key":"9370_CR35","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P Liberatore","year":"2005","unstructured":"Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203\u2013232 (2005)","journal-title":"Artif. Intell."},{"key":"9370_CR36","volume-title":"Automated Theorem Proving: A Logical Basis","author":"DW Loveland","year":"1978","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Noth-Holland, Amsterdam (1978)"},{"key":"9370_CR37","doi-asserted-by":"crossref","unstructured":"Lynce, I., Marques-Silva, J.: Probing-based preprocessing techniques for propositional satisfiability. In: Proceedings ICTAI\u201903, pp. 105\u2013110 (2003)","DOI":"10.1109\/TAI.2003.1250177"},{"key":"9370_CR38","doi-asserted-by":"crossref","unstructured":"Manthey, N.: Coprocessor 2.0 \u2014a flexible CNF simplifier\u2014(tool presentation). In: Proceedings of SAT\u201912, pp. 436\u2013441 (2012)","DOI":"10.1007\/978-3-642-31612-8_34"},{"key":"9370_CR39","unstructured":"Manthey, N.: Solver Description of RISS 2.0 and PRISS 2.0. Technical report, TU Dresden, Knowledge Representation and Reasoning (2012)"},{"key":"9370_CR40","unstructured":"Marques, J.P.: Silva and K.A. Sakallah. GRASP\u2014 a new search algorithm for satisfiability. In Proceedings of ICCAD\u201996, pp. 220\u2013227 (1996)"},{"key":"9370_CR41","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1038\/22055","volume":"33","author":"R Monasson","year":"1999","unstructured":"Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic \u2018phase transitions\u2019. Nature 33, 133\u2013137 (1999)","journal-title":"Nature"},{"key":"9370_CR42","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S. (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of DAC\u201901, pp. 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"9370_CR43","doi-asserted-by":"crossref","unstructured":"Muise, C.J., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: fast d-DNNF compilation with sharpSAT. In: Proceedings of AI\u201912, pp. 356\u2013361 (2012)","DOI":"10.1007\/978-3-642-30353-1_36"},{"key":"9370_CR44","doi-asserted-by":"crossref","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Proceedings of CP\u201902, pp. 185\u2013199 (2002)","DOI":"10.1007\/3-540-46135-3_13"},{"key":"9370_CR45","unstructured":"Palacios, H., Bonet, B., Darwiche, A., Geffner, H.: Pruning conformant plans by counting models on compiled d-DNNF representations. In: Proceedings of ICAPS\u201905, pp. 141\u2013150 (2005)"},{"key":"9370_CR46","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Vivifying propositional clausal formulae. In: Proceedings of ECAI\u201908, pp. 525\u2013529 (2008)"},{"issue":"1","key":"9370_CR47","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0095-8956(84)90013-3","volume":"36","author":"N Robertson","year":"1984","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J. Comb. Theory Ser. B 36(1), 49\u201364 (1984)","journal-title":"J. Comb. Theory Ser. B"},{"issue":"1\u20132","key":"9370_CR48","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(94)00092-1","volume":"82","author":"D Roth","year":"1996","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artif. Intell. 82(1\u20132), 273\u2013302 (1996)","journal-title":"Artif. Intell."},{"issue":"1","key":"9370_CR49","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.jda.2009.06.002","volume":"8","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50\u201364 (2010)","journal-title":"J. Discrete Algorithms"},{"key":"9370_CR50","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proceedings of SAT\u201904 (2004)"},{"key":"9370_CR51","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: Proceedings of AAAI\u201905, pp. 475\u2013482 (2005)"},{"key":"9370_CR52","unstructured":"Subbarayan, S., Bordeaux, L., Hamadi, Y.: Knowledge compilation properties of tree-of-BDDs. In Proceedings of AAAI\u201907, pp. 502\u2013507 (2007)"},{"key":"9370_CR53","doi-asserted-by":"crossref","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: non increasing variable elimination resolution for preprocessing SAT instances. In: Proceedings of SAT\u201904, pp. 276\u2013291 (2004)","DOI":"10.1007\/11527695_22"},{"key":"9370_CR54","doi-asserted-by":"crossref","unstructured":"Thurley, M.: SharpSAT\u2014counting models with advanced component caching and implicit BCP. In: Proceedings of SAT\u201906, pp. 424\u2013429 (2006)","DOI":"10.1007\/11814948_38"},{"key":"9370_CR55","doi-asserted-by":"crossref","unstructured":"Toda, T., Tsuda, K.: BDD construction for all solutions SAT and efficient caching mechanism. In: Proceedings of SAC\u201915, Track on Constraint Solving and Programming and Knowledge Representation and Reasoning (CSP-KR) (2015)","DOI":"10.1145\/2695664.2695941"},{"issue":"1","key":"9370_CR56","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239\u2013253 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9370_CR57","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0304-3975(79)90044-6","volume":"8","author":"LG Valiant","year":"1979","unstructured":"Valiant, L.G.: The complexity of computing the permanent. Theor. Comput. Sci. 8, 189\u2013201 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"9370_CR58","first-page":"166","volume":"96","author":"H Zhang","year":"1996","unstructured":"Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. Proc. ISAIM 96, 166\u2013169 (1996)","journal-title":"Proc. ISAIM"},{"key":"9370_CR59","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Proceedings of ICCAD\u201901, pp. 279\u2013285 (2001)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9370-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9370-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9370-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9370-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T06:54:19Z","timestamp":1748847259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9370-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,7]]},"references-count":59,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["9370"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9370-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,7]]}}}