{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T20:17:59Z","timestamp":1740169079509,"version":"3.37.3"},"reference-count":26,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61672261","61502199","61402196","61373052"],"award-info":[{"award-number":["61672261","61502199","61402196","61373052"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2018]]},"DOI":"10.1109\/access.2018.2855739","type":"journal-article","created":{"date-parts":[[2018,7,13]],"date-time":"2018-07-13T18:43:41Z","timestamp":1531507421000},"page":"41042-41049","source":"Crossref","is-referenced-by-count":0,"title":["A Parallel Extension Rule-Based Algorithm for #SAT Problem Using Model-Counting Tree"],"prefix":"10.1109","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-4718","authenticated-orcid":false,"given":"Naiyu","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dantong","family":"Ouyang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fengyu","family":"Jia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liming","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"279","article-title":"Efficient conflict driven learning in a Boolean satisfiability solver","author":"zhang","year":"2001","journal-title":"Proc Int Conf Comput Aided Design"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref12","first-page":"243","article-title":"Fast probabilistic planning through weighted model counting","author":"domshlak","year":"2006","journal-title":"Proceedings of 16th ICAPS"},{"key":"ref13","first-page":"475","article-title":"Solving Bayesian networks by weighted model counting","author":"sang","year":"2005","journal-title":"Proc 20th Nat Conf Artif Intell"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"ref15","first-page":"217","article-title":"New worst-case upper bound for #2-SAT and #3-SAT with the number of clauses as the parameter","author":"zhou","year":"2010","journal-title":"Proc 24th Nat Conf Artif Intell"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/11499107_24","article-title":"A new approach to model counting","author":"wei","year":"2005","journal-title":"Proc Int Conf Theory Appl Satisfiability Test"},{"key":"ref17","first-page":"2293","article-title":"From sampling to model counting","author":"gomes","year":"2007","journal-title":"Proc 20th Int Joint Conf Artif Intell"},{"key":"ref18","first-page":"54","article-title":"Model counting: A new strategy for obtaining good bounds","author":"gomes","year":"2006","journal-title":"Proc 21th Nat Conf Artif Intell"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10479-009-0680-7"},{"key":"ref4","first-page":"2703","article-title":"Double configuration checking in stochastic local search for satisfiability","author":"luo","year":"2014","journal-title":"Proc 28th AAAI Conf Artif Intell"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_31"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1145\/309847.309942","article-title":"Symbolic model checking using SAT procedures instead of BDDs","author":"biere","year":"1999","journal-title":"Proc 36rd ACM\/IEEE Design Automat Conf"},{"key":"ref5","first-page":"489","article-title":"Comprehensive score: Towards efficient local search for SAT with long clauses","author":"cai","year":"2013","journal-title":"Proc 23th Int Joint Conf Artif Intel"},{"key":"ref8","first-page":"318","article-title":"Unifying SAT-based and graph-based planning","author":"kautz","year":"1999","journal-title":"Proc 16th Int Joint Conf Artif Intell"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.858352"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(03)00204-X"},{"key":"ref9","first-page":"186","article-title":"Faulty interaction identification via constraint solving and optimization","author":"zhang","year":"2012","journal-title":"Proc Int Conf Theory Appl Satisfiability Test"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02917402"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1613\/jair.601","article-title":"The good old Davis–Putnam procedure helps counting models","volume":"10","author":"birnbaum","year":"1999","journal-title":"J Artif Intell Res"},{"key":"ref22","first-page":"20","article-title":"Combining component caching and clause learning for effective model counting","author":"sang","year":"2004","journal-title":"Proc Int Conf Theory Appl Satisfiability Test"},{"key":"ref21","first-page":"157","article-title":"Counting models using connected components","author":"bayardo","year":"2000","journal-title":"Proc 17th Nat Conf Artif Intell"},{"key":"ref24","first-page":"670","article-title":"Towards efficient sampling: Exploiting random walk strategies","author":"wei","year":"2004","journal-title":"Proc 19th Nat Conf Artif Intell"},{"key":"ref23","first-page":"1916","article-title":"Counting models using extension rules","author":"yin","year":"2007","journal-title":"Proc 22nd Nat Conf Artif Intell"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027339205632"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8274985\/08410871.pdf?arnumber=8410871","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,3]],"date-time":"2023-09-03T18:57:41Z","timestamp":1693767461000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8410871\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/access.2018.2855739","relation":{},"ISSN":["2169-3536"],"issn-type":[{"type":"electronic","value":"2169-3536"}],"subject":[],"published":{"date-parts":[[2018]]}}}