{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T16:45:27Z","timestamp":1745426727717},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_17","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"195-210","source":"Crossref","is-referenced-by-count":53,"title":["A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piergiorgio","family":"Bertoli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Korni\u0142owicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur. Timed Automata. In Proc. 11th International Computer Aided Verification Conference, pages 8\u201322, 1999.","DOI":"10.1007\/3-540-48683-6_3"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"A. Armando, C. Castellini, and E. Giunchiglia. SAT-based procedures for temporal reasoning. In Proc. European Conference on Planning, ECP-99, 1999.","DOI":"10.1007\/10720246_8"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"G. Audemard, A. Cimatti, A. Korni!lowicz, and R. Sebastiani. Bounded Model Checking for Timed Systems. Technical Report 0201-05, ITC-IRST, Trento, Italy, January 2002. Submitted for publication.","DOI":"10.1007\/3-540-36135-9_16"},{"key":"17_CR4","unstructured":"R. J. Bayardo, Jr. and R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT instances. In Proc AAAI\u201997, pages 203\u2013208. AAAI Press, 1997."},{"key":"17_CR5","unstructured":"Michel Berkelaar. The solver lpsolve for Linear Programming and Mixed-Integer Problems. Available at http:\/\/elib.zib.de\/pub\/Packages\/mathprog\/linprog\/lp-solve\/ ."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV\u201999, 1999.","DOI":"10.21236\/ADA360973"},{"key":"17_CR7","volume-title":"Technical Report 110","author":"M. Buro","year":"1992","unstructured":"M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992."},{"issue":"2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B. V. Cherkassky","year":"1999","unstructured":"Boris V. Cherkassky and Andrew V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, 85(2):277\u2013311, 1999.","journal-title":"Mathematical Programming"},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"A. Cimatti","year":"2002","unstructured":"A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In Proc. 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of LNCS Springer, 2002."},{"key":"17_CR10","unstructured":"E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. In Proc. AAAI\u201998, pages 948\u2013953, 1998."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano, A. Tacchella, and M. Vardi. Towards an Efficient Library for SAT: a Manifesto. In Proc. SAT 2001, Electronics Notes in Discrete Mathematics. Elsevier Science., 2001.","DOI":"10.1016\/S1571-0653(04)00329-4"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. CADE13, LNAI. Springer Verlag, August 1996.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K(m). Information and Computation, 162(1\/2), October\/November 2000.","DOI":"10.1006\/inco.1999.2850"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"I. Horrocks and P. F. Patel-Schneider. FaCT and DLP. In Proc. of Tableaux\u201998, number 1397 in LNAI, pages 27\u201330. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-69778-0_5"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"J. Moeller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. In Electronic Notes in Theoretical Computer Science, volume 23. Elsevier Science, 2001.","DOI":"10.1016\/S1571-0661(04)80671-6"},{"key":"17_CR16","unstructured":"R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001."},{"key":"17_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u20192000","author":"O. Shtrichmann","year":"2000","unstructured":"Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV\u20192000, volume 1855 of LNCS. Springer, 2000."},{"key":"17_CR18","unstructured":"K. Stergiou and M. Koubarakis. Backtracking algorithms for disjunctions of temporal constraints. In Proc. AAAI, pages 248\u2013253, 1998."},{"key":"17_CR19","unstructured":"S. Wolfman and D. Weld. The LPSAT Engine & its Application to Resource Planning. In Proc. IJCAI, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T16:36:31Z","timestamp":1629563791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}