{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T14:03:11Z","timestamp":1751032991610,"version":"3.37.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,11,10]],"date-time":"2009-11-10T00:00:00Z","timestamp":1257811200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s10009-009-0133-2","type":"journal-article","created":{"date-parts":[[2009,11,9]],"date-time":"2009-11-09T07:40:17Z","timestamp":1257752417000},"page":"23-37","source":"Crossref","is-referenced-by-count":2,"title":["Don\u2019t care in SMT: building flexible yet efficient abstraction\/refinement solvers"],"prefix":"10.1007","volume":"12","author":[{"given":"Andreas","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Schallhart","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,11,10]]},"reference":[{"key":"133_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp 2\u201322 (2005)","DOI":"10.1007\/11591191_2"},{"key":"133_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Computer Aided Verification (CAV), pp 515\u2013518 (2004)","DOI":"10.1007\/978-3-540-27813-9_49"},{"key":"133_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, A.: Simplifying diagnosis using LSAT: a propositional approach to reasoning from first principles. In: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR), pp 49\u201363 (2005)","DOI":"10.1007\/11493853_6"},{"key":"133_CR4","unstructured":"Bauer, A., Leucker, M., Schallhart, C., Tautschnig, M.: Don\u2019t care in SMT\u2014building flexible yet efficient abstraction\/refinement solvers. In: Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA\u201907), France, RNTI, Revue des Nouvelles Technologies de l\u2019Information (2007a)"},{"key":"133_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: Design, Automation and Test in Europe (DATE), pp 924\u2013929 (2007b)","DOI":"10.1109\/DATE.2007.364411"},{"key":"133_CR6","doi-asserted-by":"crossref","unstructured":"Belov, A., Stachniak, Z.: Substitutional definition of satisfiability in classical propositional logic. In: Theory and Applications of Satisfiability Testing (SAT), pp 31\u201345 (2005)","DOI":"10.1007\/11499107_3"},{"key":"133_CR7","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp 317\u2013333 (2005)","DOI":"10.1007\/978-3-540-31980-1_21"},{"issue":"1","key":"133_CR8","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/BF02136174","volume":"18","author":"J.P. Delgrande","year":"1996","unstructured":"Delgrande J.P., Gupta A.: The complexity of minimum partial truth assignments and implication in negation-free formulae. Ann. Math. Artif. Intell. 18(1), 51\u201367 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"133_CR9","unstructured":"DIMACS: Satisfiability: Suggested format. Tech. rep. (1993)"},{"key":"133_CR10","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification (CAV), pp 81\u201394 (2006)","DOI":"10.1007\/11817963_11"},{"key":"133_CR11","doi-asserted-by":"crossref","unstructured":"Een, N., S\u00f6rensson, N.: An extensible sat-solver. In: Theory and Application of Satisfiability Testing (SAT), pp 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"133_CR12","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Computer Aided Verification (CAV), pp 175\u2013188 (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"issue":"9","key":"133_CR13","first-page":"1305","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs N., Caspi P., Raymond P., Pilaud D.: The synchronous dataflow programming language. Lustre 79(9), 1305\u20131320 (1991)","journal-title":"Lustre"},{"key":"133_CR14","doi-asserted-by":"crossref","unstructured":"Jones, R.B., Dill, D.L.: Automatic verification of pipelined microprocessors control. In: Computer Aided Verification (CAV), pp 68\u201380 (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"issue":"1","key":"133_CR15","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/S0890-5401(03)00037-3","volume":"187","author":"L.M. Kirousis","year":"2003","unstructured":"Kirousis L.M., Kolaitis P.G.: The complexity of minimal satisfiability problems. Inf. Comput. 187(1), 20\u201339 (2003)","journal-title":"Inf. Comput."},{"key":"133_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Computer Aided Verification (CAV), pp 424\u2013437 (2006)","DOI":"10.1007\/11817963_39"},{"issue":"1","key":"133_CR17","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1147\/rd.471.0057","volume":"47","author":"R. Lougee-Heimer","year":"2003","unstructured":"Lougee-Heimer R.: The common optimization interface for operations research: promoting open-source software in the operations research community. IBM. J. Res. Dev. 47(1), 57\u201366 (2003)","journal-title":"IBM. J. Res. Dev."},{"key":"133_CR18","unstructured":"Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: Proceedings of the Ninth International Symposium on Artificial Intelligence and Mathematics (2006)"},{"key":"133_CR19","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design (ICCAD), pp 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"133_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC), pp 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"133_CR21","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad M.R., Biere A., Gupta A.: A survey of recent advances in sat-based formal verification. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Softw. Tools Technol. Transf."},{"key":"133_CR22","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Techical report, Department of Computer Science, University of Iowa, http:\/\/www.SMT-LIB.org (2006)"},{"issue":"1","key":"133_CR23","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.ic.2005.08.001","volume":"204","author":"Y. Rodeh","year":"2006","unstructured":"Rodeh Y., Strichman O.: Building small equality graphs for deciding equailty logic with uninterpreted functions. Inf. Comput. 204(1), 26\u201359 (2006)","journal-title":"Inf. Comput."},{"key":"133_CR24","doi-asserted-by":"crossref","unstructured":"Roorda, J.W., Claessen, K.: SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Computer Aided Verification (CAV), pp 175\u2013189 (2006)","DOI":"10.1007\/11817963_19"},{"key":"133_CR25","doi-asserted-by":"crossref","unstructured":"Rushby, J: Harnessing disruptive innovation in formal verification. In: Softw. Eng. Formal Methods, pp 21\u201330 (2006a)","DOI":"10.1109\/SEFM.2006.24"},{"key":"133_CR26","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Tutorial: automated formal methods with PVS, SAL, and Yices. In: Software Engineering and Formal Methods (SEFM), p 262 (2006b)","DOI":"10.1109\/SEFM.2006.37"},{"key":"133_CR27","doi-asserted-by":"crossref","unstructured":"Sheini, H., Sakallah, K.: From propositional satisfiability to satisfiability modulo theories. In: Theory and Applications of Satisfiability Testing (SAT), pp 1\u20139 (2006)","DOI":"10.1007\/11814948_1"},{"key":"133_CR28","doi-asserted-by":"crossref","unstructured":"Sheini, H.M., Sakallah, K.A.: A scalable method for solving satisfiability of integer linear arithmetic logic. In: Theory and Application of Satisfiability Testing (SAT), pp 241\u2013256 (2005)","DOI":"10.1007\/11499107_18"},{"issue":"4","key":"133_CR29","doi-asserted-by":"crossref","first-page":"769","DOI":"10.1145\/322276.322288","volume":"28","author":"R. Shostak","year":"1981","unstructured":"Shostak R.: Deciding linear inequalities by computing loop residues. J. ACM 28(4), 769\u2013779 (1981)","journal-title":"J. ACM"},{"issue":"1","key":"133_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1137\/S1052623403426556","volume":"16","author":"A. W\u00e4chter","year":"2005","unstructured":"W\u00e4chter A., Biegler L.T.: Line search filter methods for nonlinear programming: motivation and global convergence. SIAM J. Optim. 16(1), 1\u201331 (2005)","journal-title":"SIAM J. Optim."},{"key":"133_CR31","unstructured":"Weber, T.: A SAT-based Sudoku solver. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Short Paper Proceedings, pp 11\u201315 (2005)"},{"key":"133_CR32","doi-asserted-by":"crossref","unstructured":"Zantema, H., Groote, J.F.: Transforming equality logic to propositional logic. Electr. Notes. Theor. Comput. Sci. 86(1) (2003)","DOI":"10.1016\/S1571-0661(04)80661-3"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0133-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0133-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0133-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T04:12:06Z","timestamp":1739419926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0133-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,10]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["133"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0133-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2009,11,10]]}}}