{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T13:59:31Z","timestamp":1723471171997},"reference-count":7,"publisher":"Association for Computing Machinery (ACM)","issue":"3\/4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Commun. Comput. Algebra"],"published-print":{"date-parts":[[2013,1,15]]},"abstract":"We propose a new decision procedure for the existential theory of the reals. It performs a backtracking search for a model in R, where the backtracking is powered by a novel conflict resolution procedure based on cylindrical algebraic decomposition. The initial experimental results are very encouraging. The full article has been accepted at the 6th International Joint Conference on Automated Reasoning (IJCAR 2012).<\/jats:p>","DOI":"10.1145\/2429135.2429155","type":"journal-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T15:28:56Z","timestamp":1358868536000},"page":"104-105","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Solving non-linear arithmetic"],"prefix":"10.1145","volume":"46","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[{"name":"New York University, New York, USA"}]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,1,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0463"},{"key":"e_1_2_1_2_1","first-page":"134","volume-title":"Automata Theory and Formal Languages","author":"Collins G. E.","year":"1975"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80152-6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/96877.96943"},{"key":"e_1_2_1_6_1","unstructured":"H. Hong. Comparison of several decision algorithms for the existential theory of the reals. 1991. H. Hong. Comparison of several decision algorithms for the existential theory of the reals. 1991."},{"key":"e_1_2_1_7_1","unstructured":"J. P. M.\n \n Silva I.\n \n Lynce and \n \n \n S.\n \n Malik\n \n \n . \n Conflict-driven clause learning SAT solvers. In A. Biere M. Heule H. van Maaren and T. Walsh editors Handbook of Satisfiability volume \n 185\n of \n Frontiers in Artificial Intelligence and Applications pages \n 131\n --\n 153\n . \n IOS Press 2009\n . J. P. M. Silva I. Lynce and S. Malik. Conflict-driven clause learning SAT solvers. In A. Biere M. Heule H. van Maaren and T. Walsh editors Handbook of Satisfiability volume 185 of Frontiers in Artificial Intelligence and Applications pages 131--153. IOS Press 2009."}],"container-title":["ACM Communications in Computer Algebra"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429135.2429155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T07:58:22Z","timestamp":1672387102000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429135.2429155"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,15]]},"references-count":7,"journal-issue":{"issue":"3\/4","published-print":{"date-parts":[[2013,1,15]]}},"alternative-id":["10.1145\/2429135.2429155"],"URL":"https:\/\/doi.org\/10.1145\/2429135.2429155","relation":{},"ISSN":["1932-2240"],"issn-type":[{"value":"1932-2240","type":"print"}],"subject":[],"published":{"date-parts":[[2013,1,15]]},"assertion":[{"value":"2013-01-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
