{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T20:10:05Z","timestamp":1756757405733,"version":"3.44.0"},"reference-count":20,"publisher":"IEEE","license":[{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1109\/iske47853.2019.9170372","type":"proceedings-article","created":{"date-parts":[[2020,8,18]],"date-time":"2020-08-18T17:10:34Z","timestamp":1597770634000},"page":"248-252","source":"Crossref","is-referenced-by-count":0,"title":["A Learned Clause Deletion Strategy Based on Distance Ratio"],"prefix":"10.1109","author":[{"given":"Meng","family":"Wang","sequence":"first","affiliation":[{"name":"Jiaotong University,School of Mathematics, Southwest,Chengdu,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xingxing","family":"He","sequence":"additional","affiliation":[{"name":"Jiaotong University,School of Mathematics, Southwest,Chengdu,China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Jiaotong University Ulster,School of Computing,Chengdu,China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"203","article-title":"Using CSP look-back techniques to solve real-world SAT instance","author":"bayardo","year":"1997","journal-title":"AAAI"},{"key":"ref11","first-page":"530","article-title":"Chaff: an efficient SAT solver","author":"malik","year":"2001","journal-title":"Proceedings of the Design Automation Conference"},{"key":"ref12","first-page":"142","author":"goldberg","year":"2002","journal-title":"BerkMin a fast and robust SAT solver Proceedings of the Design Automation and Test"},{"key":"ref13","first-page":"502","article-title":"An extensible sat solver","author":"e\u00e9n","year":"2003","journal-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_16"},{"key":"ref15","first-page":"51","article-title":"Plingeling and Treengeling entering the SAT Competition 2013","author":"lingeling","year":"2013","journal-title":"Proc SAT Competition"},{"key":"ref16","article-title":"Revisiting the learnd clauses database reduction strategies","author":"jabbour","year":"2014","journal-title":"arXiv 1402 1956"},{"key":"ref17","article-title":"Towards learnt clauses database reduction strategies based on dominance relationship","author":"lonlac","year":"2017","journal-title":"arXiv 1705 10898"},{"key":"ref18","first-page":"30","article-title":"A learnt clauses reduction strategy based on length of resolution","volume":"54","author":"chang","year":"2018","journal-title":"Computer Engineering and Applications"},{"key":"ref19","first-page":"138","article-title":"A clause evaluation algorithm base on the trend strength","volume":"45","author":"chen","year":"2018","journal-title":"Computer Science"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_8"},{"key":"ref3","first-page":"399","article-title":"Predicting learnt clauses quality in modern sat solvers","author":"audemard","year":"2009","journal-title":"Proceedings of the International Joint Conference on Artificial Intelligence"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref5","first-page":"23","author":"guojun","year":"2007","journal-title":"Introduction and summarization principle of mathematical logic"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref2","first-page":"220","article-title":"GRASP: a new search algorithm for satisfiability","author":"silva","year":"2002","journal-title":"Proceedings of the IEEE ACM International Conference on Computer-Aided Design"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017434"},{"key":"ref20","article-title":"Efficient Conflict Driven Learning in a Boolean Satisfiability Solver","author":"zhang","year":"2001","journal-title":"Int Conf Comput -Aided Design"}],"event":{"name":"2019 IEEE 14th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)","start":{"date-parts":[[2019,11,14]]},"location":"Dalian, China","end":{"date-parts":[[2019,11,16]]}},"container-title":["2019 IEEE 14th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9163188\/9170202\/09170372.pdf?arnumber=9170372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T19:29:24Z","timestamp":1756754964000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9170372\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/iske47853.2019.9170372","relation":{},"subject":[],"published":{"date-parts":[[2019,11]]}}}