{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T05:27:42Z","timestamp":1729661262868,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/hldvt.2004.1431255","type":"proceedings-article","created":{"date-parts":[[2008,7,18]],"date-time":"2008-07-18T15:07:52Z","timestamp":1216393672000},"page":"129-134","source":"Crossref","is-referenced-by-count":0,"title":["CNF formula simplification using implication reasoning"],"prefix":"10.1109","author":[{"family":"Rajat Arora","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.S.","family":"Hsiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2004.1261028"},{"key":"17","article-title":"NIVER: Non increasing variable elimination resolution for preprocessing SAT instances","author":"subbarayan","year":"2004","journal-title":"Proc SAT'04"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"15","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"Proceedings of (TACAS) Conference"},{"key":"16","first-page":"283","author":"hoos","year":"2000","journal-title":"Satlib An online resource for research on sat"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2003.1219133"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2003.1252476"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.1999.761110"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"year":"0","key":"20"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"1","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A search algorithm for prepositional satisfiability","volume":"48","author":"marques-silva","year":"1999","journal-title":"IEEE Transaction on Computers"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/54.867894"},{"key":"7","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1109\/TAI.2003.1250177","article-title":"Probing-based preprocessing techniques for prepositional satisfiability","author":"lynce","year":"2003","journal-title":"IEEE Int l Conf Tools with Artificial Intelligence"},{"key":"6","first-page":"341","article-title":"Effective preprocessing with hyper resolution and equality reduction","author":"bacchus","year":"0","journal-title":"Lectures Notes in Computer Science Theory and Applications of Satisfiability Testing 6th International Conference SAT 2003"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCB.2002.805807"},{"key":"4","article-title":"Exploiting the real power of unit propagation lookahead","author":"berre","year":"2001","journal-title":"LICS workshop on Theory and Applications of Satisfiability Testing (SAT 2001)"},{"year":"0","key":"9"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253706"}],"event":{"name":"Proceedings. Ninth IEEE International High-Level Design Validation and Test Workshop (IEEE Cat. No.04EX940)","start":{"date-parts":[[2004,11,10]]},"location":"Sonoma Valley, CA, USA","end":{"date-parts":[[2004,11,12]]}},"container-title":["Proceedings. Ninth IEEE International High-Level Design Validation and Test Workshop (IEEE Cat. No.04EX940)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9785\/30870\/01431255.pdf?arnumber=1431255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,18]],"date-time":"2017-06-18T10:01:44Z","timestamp":1497780104000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1431255\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/hldvt.2004.1431255","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}