{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:43:34Z","timestamp":1725529414765},"reference-count":13,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/date.2004.1268823","type":"proceedings-article","created":{"date-parts":[[2004,6,21]],"date-time":"2004-06-21T21:52:40Z","timestamp":1087854760000},"page":"30-35","source":"Crossref","is-referenced-by-count":3,"title":["Arithmetic reasoning in DPLL-based SAT solving"],"prefix":"10.1109","author":[{"given":"M.","family":"Wedler","sequence":"first","affiliation":[]},{"given":"D.","family":"Stoffel","sequence":"additional","affiliation":[]},{"given":"W.","family":"Kunz","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2001.915055"},{"key":"11","article-title":"Arithemetik reasoning in dpll-based sat solving","author":"wedler","year":"2003","journal-title":"Technical Report EIS-11-03-1"},{"key":"12","article-title":"Functional test generation using constraint logic programming","author":"zeng","year":"2001","journal-title":"Proc IFIP International Conference on Very Large Scale Integration (IFIP VLSI-SOC 2001)"},{"key":"3","article-title":"Rtl-datapath verifi cation using integer linear programming","author":"brinkmann","year":"2002","journal-title":"Proc Asia and South Pacifi C Design Automation Conference (ASPDAC-02)"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968616"},{"key":"1","first-page":"195","article-title":"A sat based approach for solving formulas over boolean and linear mathematical propositions","author":"audemard","year":"2002","journal-title":"Conference on Automated Deduction (CADE"},{"key":"7","article-title":"Formal verifi cation on the RT level computing one-to-one design abstractions by signal width reduction","author":"johannsen","year":"2001","journal-title":"IFIP International Conference on Very Large Scale Integration VLSI-SOC"},{"key":"6","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/3-540-44585-4_35","article-title":"Booster: Speeding up rtl property checking of digital designs by word-level abstraction","author":"johannsen","year":"2001","journal-title":"Proc Intl Conf Computer Aided Verifi cation(CAV-01)"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/43.936380"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776041"},{"key":"9","first-page":"1","article-title":"Layout driven synthesis of data path circuits using arithmetic reasoning","author":"neumann","year":"2003","journal-title":"Proc International Workshop on Logic and Synthesis"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"}],"event":{"name":". Design, Automation and Test in Europe Conference and Exhibition","acronym":"DATE-04","location":"Paris, France"},"container-title":["Proceedings Design, Automation and Test in Europe Conference and Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8959\/28390\/01268823.pdf?arnumber=1268823","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T08:12:14Z","timestamp":1497600734000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1268823\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":13,"URL":"https:\/\/doi.org\/10.1109\/date.2004.1268823","relation":{},"subject":[]}}