{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:08:23Z","timestamp":1784844503673,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141850","type":"print"},{"value":"9783642141867","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_26","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:20:37Z","timestamp":1278613237000},"page":"306-312","source":"Crossref","is-referenced-by-count":12,"title":["Two Techniques for Minimizing Resolution Proofs"],"prefix":"10.1007","author":[{"given":"Scott","family":"Cotton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.05.025","volume":"185","author":"H. Amjad","year":"2007","unstructured":"Amjad, H.: Compressing propositional refutations. Electron. Notes Theor. Comput. Sci.\u00a0185, 3\u201315 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Amjad, H.: Data compression for proof replay. J. of Automated Reasoning (December 2008)","DOI":"10.1007\/s10817-008-9109-2"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: HVC, pp. 114\u2013128 (2008)","DOI":"10.1007\/978-3-642-01702-5_14"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Understanding the Power of Clause Learning. J. of Artificial Intelligence Research (2004)","DOI":"10.1613\/jair.1410"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Ben-sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. of the ACM, 517\u2013526 (2001)","DOI":"10.1145\/375827.375835"},{"key":"26_CR6","unstructured":"Biere, A.: tracecheck, http:\/\/fmv.jku.at\/booleforce\/index.html"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A.: Picosat essentials. J. on Satisfiability, Boolean Modeling, and Computation, 75\u201397 (2008)","DOI":"10.1007\/978-0-387-30162-4_53"},{"key":"26_CR8","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago (1937)"},{"key":"26_CR9","unstructured":"Cotton, S.: On Some Problems in Satisfiability Solving. PhD thesis, University Joseph Fourier, Grenoble I (2009)"},{"key":"26_CR10","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat: A SAT Solver with Conflict-clause Minimization. In: Theory and Applications of Satisfiability Testing, SAT (2005)"},{"key":"26_CR11","unstructured":"Ganai, M.K., Kuehlmann, A.: On-the-fly compression of logical circuits. In: International Workshop on Logic Synthesis (2000)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-72788-0_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Gelder Van","year":"2007","unstructured":"Van Gelder, A.: Verifying propositional unsatisfiability: Pitfalls to avoid. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 328\u2013333. Springer, Heidelberg (2007)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-02777-2_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Gelder Van","year":"2009","unstructured":"Van Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 141\u2013146. Springer, Heidelberg (2009)"},{"key":"26_CR14","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for cnf formulas. In: Design, Automation and Test in Europe, DATE (2003)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"K\u00fcchlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. J. Automated Reasoning\u00a024(1-2) (February 2000)","DOI":"10.1023\/A:1006370506164"},{"key":"26_CR16","unstructured":"Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: Theory and Applications of Satisfiability Testing, SAT (2004)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. Tools and Algorithms for the Construction and Analysis of Systems, 2\u201317 (2003)","DOI":"10.1007\/3-540-36577-X_2"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-75867-9_69","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2007","author":"C. Sinz","year":"2007","unstructured":"Sinz, C.: Compressing propositional proofs by common subproof extraction. In: Moreno D\u00edaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol.\u00a04739, pp. 547\u2013555. Springer, Heidelberg (2007)"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. Artif. Intell. Eng. Des. Anal. Manuf.\u00a017 (2003)","DOI":"10.1017\/S0890060403171065"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"key":"26_CR23","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Theory and Applications of Satisfiability Testing, SAT (2003)"},{"key":"26_CR24","unstructured":"Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe, DATE (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:31:33Z","timestamp":1559241093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}