{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T23:10:39Z","timestamp":1740265839706,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540262763"},{"type":"electronic","value":"9783540316794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11499107_14","type":"book-chapter","created":{"date-parts":[[2010,7,14]],"date-time":"2010-07-14T21:56:25Z","timestamp":1279144585000},"page":"187-202","source":"Crossref","is-referenced-by-count":8,"title":["Optimizations for Compiling Declarative Models into Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Darko","family":"Marinov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suhabe","family":"Bugrara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lintao","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Adjie-Winoto, W., Schwartz, E., Balakrishnan, H., Lilley, J.: The design and implementation of an intentional naming system. In: Proc. 17th ACM Symposium on Operating Systems Principles (SOSP), Kiawah Island (December 1999)","DOI":"10.1145\/319151.319164"},{"key":"14_CR2","volume-title":"Compilers: Principles, Techniques and Tools","author":"A.V. Aho","year":"1988","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1988)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Conference on Design Automation (DAC), New Orleans, LA (June 1999)","DOI":"10.1145\/309847.309942"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"14_CR5","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, Cambridge (1990)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Edwards, J., Jackson, D., Torlak, E., Yeung, V.: Faster constraint solving with subtypes. In: Proc. International Symposium on Software Testing and Analysis (ISSTA) (July 2004)","DOI":"10.1145\/1007512.1007544"},{"key":"14_CR7","unstructured":"Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SAT-compilation of planning problems. In: IJCAI 1997, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, Nagoya, Japan, August 1997, pp. 1169\u20131176 (1997)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Zhang, L., Ashar, P., Gupta, A., Malik, S.: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: Proc. 39th Conference on Design Automation (DAC), June 2002, pp. 747\u2013750 (2002)","DOI":"10.1145\/513918.514105"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first-order relational logic. In: Proc. 8th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), San Diego, CA (November 2000)","DOI":"10.1145\/355045.355063"},{"key":"14_CR10","unstructured":"Jackson, D.: Micromodels of software: Modelling and analysis with Alloy (2001), http:\/\/sdg.lcs.mit.edu\/alloy\/book.pdf"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/3-540-45500-0_25","volume-title":"Theoretical Aspects of Computer Software","author":"D. Jackson","year":"2001","unstructured":"Jackson, D., Fekete, A.: Lightweight analysis of object interactions. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, p. 492. Springer, Heidelberg (2001)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: ALCOA: The Alloy constraint analyzer. In: Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland (June 2000)","DOI":"10.1145\/337180.337616"},{"key":"14_CR13","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Proc. European Conference on Artificial Intelligence (ECAI), Vienna, Austria (August 1992)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: Proc. 15th IEEE International Conference on Automated Software Engineering (ASE), Grenoble, France (September 2000)","DOI":"10.1109\/ASE.2000.873646"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-24605-3_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 272\u2013286. Springer, Heidelberg (2004)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Lynce, I., Marques-Silva, J.P.: Probing-based preprocessing techniques for propositional satisfiability. In: Proc. the IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2003) (November 2003)","DOI":"10.1109\/TAI.2003.1250177"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Glass, T.: Combinational equivalence checking using satisfiability and recursive learning. In: Proc. the IEEE\/ACM Design, Automation and Testing in Europe (DATE), March 2003, pp. 145\u2013149 (2003)","DOI":"10.1109\/DATE.1999.761110"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 39th Design Automation Conference (DAC) (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"14_CR19","unstructured":"Narain, S.: Network configuration management via model finding. Internal report, Telcordia Research, Piscataway, NJ (September 2004)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proc. 40th Conference on Design Automation (DAC), June 2003, pp. 425\u2013430 (2003)","DOI":"10.1145\/775832.775945"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. In: Proc. Workshop on Theory and Applications of Satisfiability Testing (June 2001)","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"I. Shlyakhter","year":"2004","unstructured":"Shlyakhter, I., Sridharan, M., Seater, R., Jackson, D.: Exploiting subformula sharing in automatic analysis of quantified formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: Non increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"14_CR24","unstructured":"Vaziri, M.: Finding Bugs Using a Constraint Solver. PhD thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology (2003)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Efficient translation of boolean formulas to CNF in formal verification of microprocessors. In: Asia and South Pacific Design Automation Conference (ASP-DAC), January 2004, pp. 310\u2013315 (2004)","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","first-page":"197","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.N. Velev","year":"2005","unstructured":"Velev, M.N.: Encoding global unobservability for efficient translation to SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 197\u2013204. Springer, Heidelberg (2005)"},{"key":"14_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 295. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11499107_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T22:31:58Z","timestamp":1740263518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11499107_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540262763","9783540316794"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11499107_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}