{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:08:00Z","timestamp":1729642080208,"version":"3.28.0"},"reference-count":12,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1109\/socc.2010.5784748","type":"proceedings-article","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T11:57:50Z","timestamp":1307707070000},"page":"177-181","source":"Crossref","is-referenced-by-count":0,"title":["A Folding Strategy for SAT solvers based on Shannon's expansion theorem"],"prefix":"10.1109","author":[{"given":"Siwat","family":"Saibua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Po-Yu","family":"Kuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dian","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming-e","family":"Jing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref4","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A Search Algorithm for Propositional Satisfiability","volume":"48","author":"marques-silva","year":"1999","journal-title":"IEEE Transactions of Computers"},{"key":"ref3","first-page":"272","article-title":"SATO: An Efficient Propositional Prover","author":"zhang","year":"1997","journal-title":"Proceedings of the International Conference on Automated Deduction"},{"key":"ref10","article-title":"Modern Techniques for Solving Boolean Satisfiability","author":"andreas","year":"2006","journal-title":"Perlen der Informatik 4"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"journal-title":"DIMACS instances","year":"0","key":"ref11"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"year":"0","key":"ref12"},{"key":"ref8","first-page":"192","author":"brayton","year":"1984","journal-title":"Logic Minimization Algorithms for VLSI Synthesis"},{"key":"ref7","first-page":"399","article-title":"Predicting Learnt Clauses Quality in Modern SAT Solvers","author":"audemard","year":"2009","journal-title":"Proceedings of the Joint International Conference for Artificial Intelligence"},{"article-title":"Improvements to Propositional Satisfiability Search Algorithms","year":"1995","author":"freeman","key":"ref2"},{"key":"ref9","first-page":"564","author":"hachtel","year":"1996","journal-title":"Logic Synthesis and Verification Algorithms"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"}],"event":{"name":"2010 IEEE International SOC Conference (SOCC)","start":{"date-parts":[[2010,9,27]]},"location":"Las Vegas, NV, USA","end":{"date-parts":[[2010,9,29]]}},"container-title":["23rd IEEE International SOC Conference"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5755492\/5784634\/05784748.pdf?arnumber=5784748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T21:25:09Z","timestamp":1497907509000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5784748\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1109\/socc.2010.5784748","relation":{},"subject":[],"published":{"date-parts":[[2010,9]]}}}