{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:47:02Z","timestamp":1743043622269,"version":"3.40.3"},"publisher-location":"Heidelberg","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319009476"},{"type":"electronic","value":"9783319009483"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-00948-3_15","type":"book-chapter","created":{"date-parts":[[2013,7,19]],"date-time":"2013-07-19T01:16:13Z","timestamp":1374196573000},"page":"231-246","source":"Crossref","is-referenced-by-count":0,"title":["Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Martin","family":"Babka","sequence":"first","affiliation":[]},{"given":"Tom\u00e1\u0161","family":"Balyo","sequence":"additional","affiliation":[]},{"given":"Jaroslav","family":"Keznikl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A. Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. International Journal on Software Tools for Technology Transfer (STTT)\u00a011(1), 69\u201383 (2009)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"15_CR2","unstructured":"Bailleux, O.: On the cnf encoding of cardinality constraints and beyond. CoRR abs\/1012.3853 (2010)"},{"key":"15_CR3","unstructured":"Bailleux, O.: Boolvar\/pb v1.0, a java library for translating pseudo-boolean constraints into cnf formulae. CoRR abs\/1103.3954 (2011)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"key":"15_CR5","first-page":"125","volume":"14","author":"J. Bieganowski","year":"2005","unstructured":"Bieganowski, J., Karatkevich, A.: Heuristics for thelen\u2019s prime implicant method. Schedae Informaticae\u00a014, 125\u2013125 (2005)","journal-title":"Schedae Informaticae"},{"key":"15_CR6","unstructured":"Biere, A.: Precosat home page (2013), \n                    http:\/\/fmv.jku.at\/precosat\/"},{"key":"15_CR7","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"issue":"4","key":"15_CR9","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1109\/TCAD.1987.1270310","volume":"6","author":"R.E. Bryant","year":"1987","unstructured":"Bryant, R.E.: Boolean analysis of mos circuits. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a06(4), 634\u2013649 (1987)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Bulej, L., Bures, T., Horky, V., Keznikl, J., Tuma, P.: Performance Awareness in Component Systems: Vision Paper. In: Proceedings of COMPSAC 2012 (2012)","DOI":"10.1109\/COMPSACW.2012.96"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Bulej, L., Bures, T., Keznikl, J., Koubkova, A., Podzimek, A., Tuma, P.: Capturing performance assumptions using stochastic performance logic. In: Proceedings of ICPE 2012 (2012)","DOI":"10.1145\/2188286.2188345"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Crama, Y., Hammer, P.L.: Boolean Functions - Theory, Algorithms, and Applications. In: Encyclopedia of Mathematics and its Applications, vol.\u00a0142. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511852008"},{"issue":"1-4","key":"15_CR14","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into sat. JSAT\u00a02(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Planes, J., Silva, J.P.M.: Iterative sat solving for minimum satisfiability. In: ICTAI, pp. 922\u2013927 (2012)","DOI":"10.1109\/ICTAI.2012.129"},{"key":"15_CR16","unstructured":"Hoos, H., Stutzle, T.: Satlib benchmark site (2013), \n                    http:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html"},{"key":"15_CR17","unstructured":"Hoos, H.H., Stutzle, T.: Satlib: An online resource for research on sat, pp. 283\u2013292. IOS Press (2000)"},{"key":"15_CR18","unstructured":"Horky, V.: Stochastic Performance Logic (SPL) Home Page (2013), \n                    http:\/\/d3s.mff.cuni.cz\/projects\/performance_evaluation\/spl\/"},{"key":"15_CR19","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI 1992: Tenth European Conference on Artificial Intelligence, Vienna, Austria, pp. 359\u2013363 (1992)"},{"key":"15_CR20","unstructured":"K\u00fcgel, A.: Homepage of Adrian K\u00fcgel (2012), \n                    http:\/\/www.uni-ulm.de\/en\/in\/institute-of-theoretical-computer-science\/m\/kuegel.html"},{"key":"15_CR21","unstructured":"Manquinho, V.: bsolo home page (2012), \n                    http:\/\/sat.inesc-id.pt\/~vmm\/research\/index.html"},{"key":"15_CR22","unstructured":"Manquinho, V., Oliveira, A., Marques-Silva, J.: Models and algorithms for computing minimum-size prime implicants. In: Proceedings of the International Workshop on Boolean Problems (1998)"},{"key":"15_CR23","unstructured":"Manquinho, V.M., Flores, P.F., Silva, J.P.M., Oliveira, A.L.: Prime implicant computation using satisfiability algorithms. In: ICTAI, pp. 232\u2013239 (1997)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-10452-7_3","volume-title":"Formal Methods: Foundations and Applications","author":"L. de Moura","year":"2009","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: An appetizer. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 23\u201336. Springer, Heidelberg (2009)"},{"issue":"1","key":"15_CR25","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0004-3702(99)00035-1","volume":"111","author":"L. Palopoli","year":"1999","unstructured":"Palopoli, L., Pirri, F., Pizzuti, C.: Algorithms for selective enumeration of prime implicants. Artificial Intelligence\u00a0111(1), 41\u201372 (1999)","journal-title":"Artificial Intelligence"},{"key":"15_CR26","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"15_CR27","unstructured":"Tompkins, D.: Ubcsat home page (2012), \n                    http:\/\/www.satlib.org\/ubcsat\/"},{"key":"15_CR28","unstructured":"Umans, C.: The minimum equivalent dnf problem and shortest implicants. In: FOCS, pp. 556\u2013563 (1998)"},{"issue":"2","key":"15_CR29","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M.N. Velev","year":"2003","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. J. Symb. Comput.\u00a035(2), 73\u2013106 (2003)","journal-title":"J. Symb. Comput."}],"container-title":["Studies in Computational Intelligence","Software Engineering Research, Management and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-00948-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T23:40:07Z","timestamp":1676331607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-00948-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319009476","9783319009483"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-00948-3_15","relation":{},"ISSN":["1860-949X","1860-9503"],"issn-type":[{"type":"print","value":"1860-949X"},{"type":"electronic","value":"1860-9503"}],"subject":[],"published":{"date-parts":[[2014]]}}}