{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:03:20Z","timestamp":1761581000602},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_30","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"394-409","source":"Crossref","is-referenced-by-count":36,"title":["Minimum Satisfying Assignments for SMT"],"prefix":"10.1007","author":[{"given":"Isil","family":"Dillig","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal Assignments for Bounded Model Checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-54507-7_12","volume-title":"Fundamentals of Artificial Intelligence Research","author":"P. Marquis","year":"1991","unstructured":"Marquis, P.: Extending Abduction from Propositional to First-Order Logic. In: Jorrand, P., Kelemen, J. (eds.) FAIR 1991. LNCS, vol.\u00a0535, pp. 141\u2013155. Springer, Heidelberg (1991)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-39724-3_5","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E., Groce, A., Strichman, O.: Predicate Abstraction with Minimum Predicates. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 19\u201334. Springer, Heidelberg (2003)"},{"key":"30_CR4","unstructured":"Silva, J.: On computing minimum size prime implicants. In: International Workshop on Logic Synthesis, Citeseer (1997)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Pizzuti, C.: Computing prime implicants by integer programming. In: IEEE International Conference on Tools with Artificial Intelligence, pp. 332\u2013336. IEEE (1996)","DOI":"10.1109\/TAI.1996.560473"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI (2012)","DOI":"10.1145\/2254064.2254087"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-15769-1_15","volume-title":"Static Analysis","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 236\u2013252. Springer, Heidelberg (2010)"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I. Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"key":"30_CR10","unstructured":"S\u00f6rensson, N., Een, N.: Minisat v1. 13-a sat solver with conflict-clause minimization. In: SAT 2005, p. 53 (2005)"},{"issue":"91-99","key":"30_CR11","first-page":"300","volume":"7","author":"D. Cooper","year":"1972","unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Intelligence\u00a07(91-99), 300 (1972)","journal-title":"Machine Intelligence"},{"issue":"1","key":"30_CR12","first-page":"187","volume":"46","author":"I. Dillig","year":"2011","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. POPL\u00a046(1), 187\u2013200 (2011)","journal-title":"POPL"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Manquinho, V., Flores, P., Silva, J., Oliveira, A.: Prime implicant computation using satisfiability algorithms. In: ICTAI, pp. 232\u2013239 (1997)","DOI":"10.1109\/TAI.1997.632261"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-540-71209-1_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2007","unstructured":"Amla, N., McMillan, K.L.: Combining Abstraction Refinement and SAT-Based Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 405\u2013419. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:56Z","timestamp":1620129596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}