{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T07:09:10Z","timestamp":1774940950755,"version":"3.50.1"},"reference-count":45,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1109\/iske.2017.8258780","type":"proceedings-article","created":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T17:47:01Z","timestamp":1516038421000},"page":"1-6","source":"Crossref","is-referenced-by-count":2,"title":["Adding a LBD-based rewarding mechanism in branching heuristic for SAT solvers"],"prefix":"10.1109","author":[{"given":"Wenjing","family":"Chang","sequence":"first","affiliation":[]},{"given":"Guanfeng","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"Understanding the power of clause learning","author":"beame","year":"2003","journal-title":"Proceedings of the 18th International Joint Conference on Artificial Intelligence"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"ref33","article-title":"Lingeling, plingeling, picosat and precosat at SAT race 2010","author":"biere","year":"2010","journal-title":"FMV Report Series Technical Report"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531077"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3023-4_7"},{"key":"ref30","article-title":"Report on a SAT competition","author":"buro","year":"1992","journal-title":"Technical Report University of Paderborn"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"ref36","author":"ryan","year":"2004","journal-title":"Efficient Algorithms for Clause Learning SAT Solvers"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_4"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/VTEST.1993.313303"},{"key":"ref40","first-page":"279","article-title":"Efficient conflict driven learning in Boolean satisfiability solver","author":"zhang","year":"2001","journal-title":"Proceedings of the International Conference on Computer Aided Design"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/43.536723"},{"key":"ref12","first-page":"1194","article-title":"Pushing the envelope: Planning, propositional logic, and stochastic search","author":"kautz","year":"1996","journal-title":"13th AAAI"},{"key":"ref13","author":"russell","year":"2002","journal-title":"Artificial Intelligence A Modern Approach"},{"key":"ref14","first-page":"208","article-title":"Randomization in backtrack search: Exploiting heavy-tailed profiles for solving hard scheduling problems","author":"gomes","year":"1998","journal-title":"4th Int Conf Art Intel Planning Syst"},{"key":"ref15","article-title":"Solving open quasigroup problems by propositional reasoning","author":"zhang","year":"1994","journal-title":"Proc Int Computer Symp"},{"key":"ref16","first-page":"394","volume":"5","author":"davis","year":"1962","journal-title":"A Machine Program for Theorem-proving Commun ACM"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref18","article-title":"Implementing the Davis-Putnam Method","author":"zhang","year":"2000","journal-title":"SAT 2000"},{"key":"ref19","first-page":"530","article-title":"Chaff: Engineering an efficient SAT solver","author":"moskewicz","year":"2001","journal-title":"Proceedings of the 38th Design Automation Conference"},{"key":"ref28","article-title":"The Quest for Efficient Boolean Satisfiability Solvers","author":"zhang","year":"2002","journal-title":"Proceedings of CADE 2002 and CAV 2002"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/43.536723"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48159-1_5"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(02)00091-3"},{"key":"ref6","article-title":"Industrial strength SAT-based alignability algorithm for hardware equivalence verification","author":"daher","year":"2007","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00097-1"},{"key":"ref5","first-page":"13","article-title":"Improved design debugging using maximum satisfiability","author":"sean","year":"2007","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref8","first-page":"669","article-title":"Solving SQL constraints by incremental translation to SAT","author":"robin","year":"2008","journal-title":"New Frontiers in Applied Artificial Intelligence"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/035\/02"},{"key":"ref2","author":"jackson","year":"2000","journal-title":"Finding Bugs with a Constraint Solver International Symposium on Software Testing and Analysis"},{"key":"ref9","article-title":"Planning as Satisfiability","author":"kautz","year":"1992","journal-title":"European Conference on Artificial Intelligence"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"key":"ref45","year":"0","journal-title":"SAT 2014 Competition web page"},{"key":"ref22","first-page":"502","article-title":"An extensible SAT-solver","author":"een","year":"2003","journal-title":"Theory and Applications of Satisfiability Testing 6th International Conference SAT 2003 Santa Margherita Ligure"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_27"},{"key":"ref42","year":"0","journal-title":"SAT 2016 Competition web page"},{"key":"ref24","article-title":"CryptoMiniSat v4","author":"soos","year":"2014","journal-title":"Sat competition"},{"key":"ref41","article-title":"Glucose3.0: Glucose in the sat 2014 competition","author":"audemard","year":"2014","journal-title":"Proceedings of SAT Competition 2014"},{"key":"ref23","first-page":"399","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"2009","journal-title":"IJCAI 2009 Proceedings of the 21st International Joint Conference on Artificial Intelligence"},{"key":"ref44","year":"0","journal-title":"SAT -Race 2015 web page"},{"key":"ref26","first-page":"275","article-title":"Using Rewarding Mechanisms for Improving Branching Heuristics","author":"carvalho","year":"2004","journal-title":"International Symposium on Theory and Applications of Satisfiability Testing"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.disopt.2006.10.012"}],"event":{"name":"2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)","location":"Nanjing","start":{"date-parts":[[2017,11,24]]},"end":{"date-parts":[[2017,11,26]]}},"container-title":["2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8246022\/8258711\/08258780.pdf?arnumber=8258780","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,2,28]],"date-time":"2018-02-28T16:55:55Z","timestamp":1519836955000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8258780\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":45,"URL":"https:\/\/doi.org\/10.1109\/iske.2017.8258780","relation":{},"subject":[],"published":{"date-parts":[[2017,11]]}}}