{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:35:36Z","timestamp":1742967336613,"version":"3.40.3"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>State-of-the-art refutation systems for SAT are largely based on the derivation of clauses meeting some redundancy criteria, ensuring their addition to a formula does not alter its satisfiability. However, there are strong propositional reasoning techniques whose inferences are not easily expressed in such systems. This paper extends the redundancy framework beyond clauses to characterize redundancy for Boolean constraints in general. We show this characterization can be instantiated to develop efficiently checkable refutation systems using redundancy properties for Binary Decision Diagrams (BDDs). Using a form of reverse unit propagation over conjunctions of BDDs, these systems capture, for instance, Gaussian elimination reasoning over XOR constraints encoded in a formula, without the need for clausal translations or extension variables. Notably, these systems generalize those based on the strong Propagation Redundancy (PR) property, without an increase in complexity.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_15","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"252-272","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Non-clausal Redundancy Properties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1282-8596","authenticated-orcid":false,"given":"Lee A.","family":"Barnett","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-Boolean constraints. Journal of Artificial Intelligence Research 45, 443\u2013480 (2012). https:\/\/doi.org\/10.1613\/jair.3653","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/BF01302964","volume":"14","author":"M Ajtai","year":"1994","unstructured":"Ajtai, M.: The complexity of the pigeonhole principle. Combinatorica 14(4), 417\u2013433 (1994). https:\/\/doi.org\/10.1007\/BF01302964","journal-title":"Combinatorica"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"SB Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Computers 27(6), 509\u2013516 (1978). https:\/\/doi.org\/10.1109\/TC.1978.1675141","journal-title":"Binary decision diagrams. IEEE Trans. Computers"},{"doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT competition 2016: Recent developments. In: Singh, S.P., Markovitch, S. (eds.) 31st AAAI Conference on Artificial Intelligence. pp. 5061\u20135063. AAAI Press (2017)","key":"15_CR4","DOI":"10.1609\/aaai.v31i1.10641"},{"doi-asserted-by":"publisher","unstructured":"Barnett, L.A., Biere, A.: Non-clausal redundancy properties (extended version). Tech. Rep. 21\/2, Johannes Kepler University Linz, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2021). https:\/\/doi.org\/10.35011\/fmvtr.2021-2","key":"15_CR5","DOI":"10.35011\/fmvtr.2021-2"},{"doi-asserted-by":"publisher","unstructured":"Barnett, L.A., Cerna, D., Biere, A.: Covered clauses are not propagation redundant. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th Intl. Joint Conference on Automated Reasoning - IJCAR. LNCS, vol. 12166, pp. 32\u201347. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_3","key":"15_CR6","DOI":"10.1007\/978-3-030-51074-9_3"},{"doi-asserted-by":"publisher","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. pp. 1267\u20131329. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017","key":"15_CR7","DOI":"10.3233\/FAIA201017"},{"unstructured":"Bayardo, R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) 14th AAAI National Conference on Artificial Intelligence. pp. 203\u2013208. AAAI Press (1997)","key":"15_CR8"},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22(1), 319\u2013351 (2004). https:\/\/doi.org\/10.1613\/jair.1410","journal-title":"Journal of Artificial Intelligence Research"},{"unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2018. pp. 13\u201314. Department of Computer Science Series of Publications B, University of Helsinki (2018)","key":"15_CR10"},{"unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)","key":"15_CR11"},{"doi-asserted-by":"publisher","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. pp. 391\u2013435. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200992","key":"15_CR12","DOI":"10.3233\/FAIA200992"},{"issue":"8","key":"15_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"publisher","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: Groote, J.F., Larsen, K.G. (eds.) 27th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS. LNCS, vol. 12651, pp. 76\u201393. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_5","key":"15_CR14","DOI":"10.1007\/978-3-030-72016-2_5"},{"doi-asserted-by":"publisher","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994). https:\/\/doi.org\/10.1109\/43.275352","key":"15_CR15","DOI":"10.1109\/43.275352"},{"doi-asserted-by":"publisher","unstructured":"Buss, S., Thapen, N.: DRAT proofs, propagation redundancy, and extended resolution. In: Janota, M., Lynce, I. (eds.) 22nd Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 11628, pp. 71\u201389. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_5","key":"15_CR16","DOI":"10.1007\/978-3-030-24258-9_5"},{"doi-asserted-by":"publisher","unstructured":"Chatalic, P., Simon, L.: Multi-resolution on compressed sets of clauses. In: 12th IEEE Intl. Conference on Tools with Artificial Intelligence - ICTAI. pp. 2\u201310. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/TAI.2000.889839","key":"15_CR17","DOI":"10.1109\/TAI.2000.889839"},{"doi-asserted-by":"publisher","unstructured":"Chew, L., Heule, M.J.H.: Sorting parity encodings by reusing variables. In: Pulina, L., Seidl, M. (eds.) 23rd Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 12178, pp. 1\u201310. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_1","key":"15_CR18","DOI":"10.1007\/978-3-030-51825-7_1"},{"issue":"1","key":"15_CR19","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods in System Design"},{"doi-asserted-by":"publisher","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) Intl. Workshop on Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 365\u2013373. Springer (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_30","key":"15_CR20","DOI":"10.1007\/3-540-52148-8_30"},{"doi-asserted-by":"publisher","unstructured":"Coudert, O., Madre, J.C.: A unified framework for the formal verification of sequential circuits. In: IEEE Intl. Conference on Computer-Aided Design - ICCAD. pp. 126\u2013129. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/ICCAD.1990.129859","key":"15_CR21","DOI":"10.1109\/ICCAD.1990.129859"},{"doi-asserted-by":"publisher","unstructured":"Coudert, O., Madre, J.C., Berthet, C.: Verifying temporal properties of sequential machines without building their state diagrams. In: Clarke, E.M., Kurshan, R.P. (eds.) 2nd Intl. Workshop on Computer Aided Verification - CAV. LNCS, vol. 531, pp. 23\u201332. Springer (1990). https:\/\/doi.org\/10.1007\/BFb0023716","key":"15_CR22","DOI":"10.1007\/BFb0023716"},{"doi-asserted-by":"publisher","unstructured":"Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: 40th Design Automation Conference - DAC. pp. 818\u2013823. ACM (2003). https:\/\/doi.org\/10.1145\/775832.776039","key":"15_CR23","DOI":"10.1145\/775832.776039"},{"doi-asserted-by":"publisher","unstructured":"Franco, J., Kouril, M., Schlipf, J., Ward, J., Weaver, S., Dransfield, M., Vanfleet, W.M.: SBSAT: a state-based, BDD-based satisfiability solver. In: Giunchiglia, E., Tacchella, A. (eds.) 6th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 2919, pp. 398\u2013410. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_30","key":"15_CR24","DOI":"10.1007\/978-3-540-24605-3_30"},{"unstructured":"Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: 10th Intl. Symposium on Artificial Intelligence and Mathematics - ISAIM (2008)","key":"15_CR25"},{"doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: 35th AAAI Conference on Artificial Intelligence. AAAI Press (2021), to appear","key":"15_CR26","DOI":"10.1609\/aaai.v35i5.16494"},{"doi-asserted-by":"publisher","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Conference on Design, Automation and Test in Europe- DATE. pp. 886\u2013891. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/DATE.2003.10008","key":"15_CR27","DOI":"10.1109\/DATE.2003.10008"},{"doi-asserted-by":"publisher","unstructured":"Goldberg, E.I., Prasad, M.R., Brayton, R.K.: Using SAT for combinational equivalence checking. In: Nebel, W., Jerraya, A. (eds.) Conference on Design, Automation and Test in Europe - DATE. pp. 114\u2013121. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/DATE.2001.915010","key":"15_CR28","DOI":"10.1109\/DATE.2001.915010"},{"issue":"1\u20132","key":"15_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1567-8326(03)00039-0","volume":"57","author":"JF Groote","year":"2003","unstructured":"Groote, J.F., Tveretina, O.: Binary decision diagrams for first-order predicate logic. J. Log. Algebraic Methods Program. 57(1\u20132), 1\u201322 (2003). https:\/\/doi.org\/10.1016\/S1567-8326(03)00039-0","journal-title":"J. Log. Algebraic Methods Program."},{"unstructured":"Heule, M., Kiesl, B.: The potential of interference-based proof systems. In: Reger, G., Traytel, D. (eds.) 1st Intl. Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements - ARCADE. EPiC Series in Computing, vol. 51, pp. 51\u201354. EasyChair (2017)","key":"15_CR30"},{"unstructured":"Heule, M.J.H., Biere, A.: All about Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, chap. Proofs for Satisfiability Problems, pp. 1\u201322. College Publications (2015)","key":"15_CR31"},{"issue":"1","key":"15_CR32","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. Journal of Artificial Intelligence Research 53(1), 127\u2013168 (2015). https:\/\/doi.org\/10.1613\/jair.4694","journal-title":"Journal of Artificial Intelligence Research"},{"doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) 26th Intl. Conference on Automated Deduction - CADE. LNCS, vol. 10395, pp. 130\u2013147. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9","key":"15_CR33","DOI":"10.1007\/978-3-319-63046-5_9"},{"doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Clausal proofs of mutilated chessboards. In: Badger, J.M., Rozier, K.Y. (eds.) 11th NASA Formal Methods Symposium - NFM. LNCS, vol. 11460, pp. 204\u2013210. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_13","key":"15_CR34","DOI":"10.1007\/978-3-030-20652-9_13"},{"doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Vojnar, T., Zhang, L. (eds.) 25th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS. LNCS, vol. 11427, pp. 41\u201358. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_3","key":"15_CR35","DOI":"10.1007\/978-3-030-17462-0_3"},{"issue":"3","key":"15_CR36","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/s10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. Journal of Automated Reasoning 64(3), 533\u2013554 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09516-0","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Strichman, O., Tzoref-Brill, R. (eds.) 13th Intl. Haifa Verification Conference - HVC. LNCS, vol. 10629, pp. 179\u2013194. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_12","key":"15_CR37","DOI":"10.1007\/978-3-319-70389-3_12"},{"doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) 19th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 9710, pp. 228\u2013245. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15","key":"15_CR38","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"15_CR39","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF02186368","volume":"12","author":"JN Hooker","year":"1988","unstructured":"Hooker, J.N.: Generalized resolution and cutting planes. Annals of Operations Research 12, 217\u2013239 (1988). https:\/\/doi.org\/10.1007\/BF02186368","journal-title":"Annals of Operations Research"},{"key":"15_CR40","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF01531033","volume":"6","author":"JN Hooker","year":"1992","unstructured":"Hooker, J.N.: Generalized resolution for 0\u20131 linear inequalities. Annals of Mathematics and Artificial Intelligence 6, 271\u2013286 (1992). https:\/\/doi.org\/10.1007\/BF01531033","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1\u20132","key":"15_CR41","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(97)83807-8","volume":"180","author":"K Hosaka","year":"1997","unstructured":"Hosaka, K., Takenaga, Y., Kaneda, T., Yajima, S.: Size of ordered binary decision diagrams representing threshold functions. Theor. Comput. Sci. 180(1\u20132), 47\u201360 (1997). https:\/\/doi.org\/10.1016\/S0304-3975(97)83807-8","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) 16th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS. LNCS, vol. 6015, pp. 129\u2013144. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10","key":"15_CR42","DOI":"10.1007\/978-3-642-12002-2_10"},{"doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, Dalea nd Sattler, U. (eds.) 6th Intl. Joint Conference on Automated Reasoning - IJCAR. LNCS, vol. 7364, pp. 355\u2013370. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","key":"15_CR43","DOI":"10.1007\/978-3-642-31365-3_28"},{"doi-asserted-by":"publisher","unstructured":"Kaiss, D., Skaba, M., Hanna, Z., Khasidashvili, Z.: Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In: 7th Intl. Conference on Formal Methods in Computer Aided Design - FMCAD. pp. 20\u201326. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.37","key":"15_CR44","DOI":"10.1109\/FAMCAD.2007.37"},{"doi-asserted-by":"publisher","unstructured":"Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: Olivetti, N., Tiwari, A. (eds.) 8th Intl. Joint Conference on Automated Reasoning - IJCAR. LNCS, vol. 9706, pp. 45\u201361. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_5","key":"15_CR45","DOI":"10.1007\/978-3-319-40229-1_5"},{"key":"15_CR46","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artificial Intelligence 224, 103\u2013118 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.03.004","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"publisher","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Yoffa, E.J., Micheli, G.D., Rabaey, J.M. (eds.) 34th Design Automation Conference - DAC. pp. 263\u2013268. ACM (1997). https:\/\/doi.org\/10.1145\/266021.266090","key":"15_CR47","DOI":"10.1145\/266021.266090"},{"key":"15_CR48","doi-asserted-by":"publisher","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 Applied Mathematics 96\u201397, 149\u2013176 (1999). https:\/\/doi.org\/10.1016\/S0166-218X(99)00037-2","journal-title":"Discrete Applied Mathematics"},{"issue":"4","key":"15_CR49","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"CY Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. The Bell System Technical Journal 38(4), 985\u2013999 (1959)","journal-title":"The Bell System Technical Journal"},{"doi-asserted-by":"publisher","unstructured":"Manthey, N.: Coprocessor 2.0 - a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) 15th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_34","key":"15_CR50","DOI":"10.1007\/978-3-642-31612-8_34"},{"doi-asserted-by":"publisher","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: IEEE Intl. Conference on Computer Aided Design - ICCAD. pp. 220\u2013227. IEEE Computer Society \/ ACM (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","key":"15_CR51","DOI":"10.1109\/ICCAD.1996.569607"},{"doi-asserted-by":"publisher","unstructured":"Motter, D.B., Markov, I.L.: A compressed breadth-first search for satisfiability. In: Mount, D.M., Stein, C. (eds.) 4th Intl. Workshop on Algorithm Engineering and Experiments - ALENEX. LNCS, vol. 2409, pp. 29\u201342. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45643-0_3","key":"15_CR52","DOI":"10.1007\/3-540-45643-0_3"},{"doi-asserted-by":"publisher","unstructured":"Olivo, O., Emerson, E.A.: A more efficient BDD-based QBF solver. In: Lee, J. (ed.) 17th Intl. Conference on Principles and Practice of Constraint Programming - CP. pp. 675\u2013690. LNCS, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_51","key":"15_CR53","DOI":"10.1007\/978-3-642-23786-7_51"},{"doi-asserted-by":"publisher","unstructured":"Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: 7th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 3542, pp. 235\u2013250. Springer (2004). https:\/\/doi.org\/10.1007\/11527695_19","key":"15_CR54","DOI":"10.1007\/11527695_19"},{"issue":"2","key":"15_CR55","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1016\/0022-0000(84)90068-0","volume":"28","author":"C Papadimitriou","year":"1984","unstructured":"Papadimitriou, C., Yannakakis, M.: The complexity of facets (and some facets of complexity). Journal of Computer and System Sciences 28(2), 244\u2013259 (1984). https:\/\/doi.org\/10.1016\/0022-0000(84)90068-0","journal-title":"Journal of Computer and System Sciences"},{"doi-asserted-by":"publisher","unstructured":"Philipp, T., Rebola-Pardo, A.: DRAT proofs for XOR reasoning. In: Michael, L., Kakas, A.C. (eds.) 15th European Conference on Logics in Artificial Intelligence - JELIA. LNCS, vol. 10021, pp. 415\u2013429 (2016). https:\/\/doi.org\/10.1007\/978-3-319-48758-8_27","key":"15_CR56","DOI":"10.1007\/978-3-319-48758-8_27"},{"doi-asserted-by":"publisher","unstructured":"Posegga, J., Lud\u00e4scher, B.: Towards first-order deduction based on Shannon graphs. In: Ohlbach, H.J. (ed.) 16th German Conference on Artificial Intelligence - GWAI. LNCS, vol. 671, pp. 67\u201375. Springer (1992). https:\/\/doi.org\/10.1007\/BFb0018993","key":"15_CR57","DOI":"10.1007\/BFb0018993"},{"doi-asserted-by":"publisher","unstructured":"Roussel, O., Manquinho, V.: Pseudo-Boolean and cardinality constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. pp. 1087\u20131129. IOS Press (2021). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-695","key":"15_CR58","DOI":"10.3233\/978-1-58603-929-5-695"},{"issue":"3","key":"15_CR59","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0020-0190(93)90256-9","volume":"48","author":"D Sieling","year":"1993","unstructured":"Sieling, D., Wegener, I.: Reduction of OBDDs in linear time. Information Processing Letters 48(3), 139\u2013144 (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90256-9","journal-title":"Information Processing Letters"},{"doi-asserted-by":"publisher","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) Computer Science - Theory and Applications, 1st Intl. Computer Science Symposium in Russia - CSR. vol. 3967, pp. 600\u2013611. Springer (2006). https:\/\/doi.org\/10.1007\/11753728_60","key":"15_CR60","DOI":"10.1007\/11753728_60"},{"doi-asserted-by":"publisher","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) 32nd Intl. Conference on Computer Aided Verification - CAV. LNCS, vol. 12224, pp. 463\u2013484. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_22","key":"15_CR61","DOI":"10.1007\/978-3-030-53288-8_22"},{"doi-asserted-by":"publisher","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) 12th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. pp. 244\u2013257. LNCS, Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24","key":"15_CR62","DOI":"10.1007\/978-3-642-02777-2_24"},{"doi-asserted-by":"publisher","unstructured":"Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Implicit state enumeration of finite state machines using BDDs. In: IEEE Intl. Conference on Computer-Aided Design - ICCAD. pp. 130\u2013133. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/ICCAD.1990.129860","key":"15_CR63","DOI":"10.1109\/ICCAD.1990.129860"},{"doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slissenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, vol. 2, pp. 115\u2013125. Steklov Mathematical Institute (1970)","key":"15_CR64","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"1","key":"15_CR65","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM 34(1), 209\u2013219 (1987). https:\/\/doi.org\/10.1145\/7531.8928","journal-title":"Journal of the ACM"},{"doi-asserted-by":"publisher","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bulletin of Symbolic Logic 1(4), 425\u2013467 (12 1995). https:\/\/doi.org\/10.2307\/421131","key":"15_CR66","DOI":"10.2307\/421131"},{"doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) 26th Intl. Conference on Computer Aided Verification - CAV. LNCS, vol. 8559, pp. 696\u2013710. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","key":"15_CR67","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"15_CR68","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0167-6377(98)00052-2","volume":"23","author":"JP Warners","year":"1998","unstructured":"Warners, J.P., Maaren, H.V., Warners, J.P., Maaren, H.V.: A two phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters 23, 81\u201388 (1998). https:\/\/doi.org\/10.1016\/S0167-6377(98)00052-2","journal-title":"Operations Research Letters"},{"doi-asserted-by":"publisher","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) 17th Intl. Conference on Theory and Applications of Satisfiability Testing - SAT. LNCS, vol. 8561, pp. 422\u2013429. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","key":"15_CR69","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:27:49Z","timestamp":1672723669000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}