{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:01:36Z","timestamp":1767772896190},"reference-count":47,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,6,1]],"date-time":"2001-06-01T00:00:00Z","timestamp":991353600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Discrete Mathematics"],"published-print":{"date-parts":[[2001,6]]},"DOI":"10.1016\/s1571-0653(04)00329-4","type":"journal-article","created":{"date-parts":[[2005,4,9]],"date-time":"2005-04-09T09:34:04Z","timestamp":1113039244000},"page":"290-310","source":"Crossref","is-referenced-by-count":3,"special_numbering":"C","title":["Towards an Efficient Library for SAT: a Manifesto"],"prefix":"10.1016","volume":"9","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Massimo","family":"Narizzano","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0653(04)00329-4_BIB1","series-title":"Proceedings of TAG AS, volume 1785 of LNCS","first-page":"411","article-title":"Symbolic Reachability Analisys Based on SAT-Solvers","author":"Abdulla","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB2","series-title":"Symbolic Model Checking without BDDs. In Proceedings of TAG AS, volume 1579 of LNCS","first-page":"193","author":"Biere","year":"1999"},{"issue":"2","key":"10.1016\/S1571-0653(04)00329-4_BIB3","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic Model Checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB4","author":"Euro","year":"1992","journal-title":"Report on a SAT competition. Technical Report 110, University of Paderborn"},{"issue":"3","key":"10.1016\/S1571-0653(04)00329-4_BIB5","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB6","series-title":"Using CSP Look-Back Techniques to Solve Real-World SAT instances, Proc. of AAAI","first-page":"203","author":"Bayardo","year":"1997"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB7","series-title":"Tractable Reasoning in Artificial Intelligence. Number 941 in LNAI.","author":"Cadoli","year":"1995"},{"issue":"4","key":"10.1016\/S1571-0653(04)00329-4_BIB8","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","article-title":"NuSMV: a new symbolic model checker","volume":"2","author":"Cimatti","year":"2000","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB9","series-title":"Proc. of CAV, LNCS.","article-title":"Benefits of Bounded Model Checking at an Industrial Setting","author":"Copty","year":"2001"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB10","author":"Castellini","year":"2001","journal-title":"SAT-based planning in complex domains: Concurrency, constraints and nondeterminism"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB11","series-title":"Introduction to Algorithms","author":"Cormen","year":"1998"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB12","series-title":"Highlights of Satisfiability Research in the Year 2000","article-title":"An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation","author":"Cadoli","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB13","unstructured":"The Second Dimacs Challenge: Satisfiability Suggested Format, ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/."},{"issue":"7","key":"10.1016\/S1571-0653(04)00329-4_BIB14","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","volume":"5","author":"Davis","year":"1962","journal-title":"Journal of the ACM"},{"issue":"90","key":"10.1016\/S1571-0653(04)00329-4_BIB15","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0004-3702(96)00040-9","article-title":"Semantics and Complexity of Abduction from Default Theories","volume":"1-2","author":"Eiter","year":"1997","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB16","series-title":"Reasoning about knowledge","author":"Fagin","year":"1995"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB17","article-title":"A Distributed Algorithm to Evaluate Quantified Boolean Formulae","author":"Feldmann","year":"2000","journal-title":"Proc. of AAAI"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB18","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","article-title":"Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem","volume":"5","author":"Franco","year":"1983","journal-title":"Discrete Applied Mathematics"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB19","series-title":"Improvements to propositional satisfiability search algorithms. PhD thesis","author":"Freeman","year":"1995"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB20","series-title":"More evaluation of decision procedures for modal logics. In Proc. of KR.","author":"Giunchiglia","year":"1998"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB21","article-title":"SAT-Based Decision Procedures for Classical Modal Logics","author":"Giunchiglia","year":"2000","journal-title":"Highlights of Satisfiability Research in the Year 2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB22","series-title":"An action language based on causal explanation: Preliminary report. In Proc. of AAAI.","author":"Giunchiglia","year":"1998"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB23","series-title":"Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proc. of IJCAR, LNCS.","author":"Giunchiglia","year":"2001"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB24","author":"Giunchiglia","year":"2001","journal-title":"Backjumping for Quantified Boolean Logic Satisfiability. In Proc. of IJCAI"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB25","author":"Giunchiglia","year":"2001","journal-title":"On the effectiveness of backjumping and trivial truth in quantified boolean formulas satisfiability. In IJCAR workshop on Theory and Application of Quantified Boolean Formulas"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB26","series-title":"Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In Proc. of CADE, LNAI.","author":"Giunchiglia","year":"1996"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB27","series-title":"Highlights of Satisfiability Research in the Year 2000","article-title":"Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems","author":"Gomes","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB28","article-title":"A Size-bounded Subset-matching cache for Satisfiability in Modal Logics","author":"Giunchiglia","year":"2000","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB29","series-title":"Highlights of Satisfiability Research in the Year 2000","article-title":"The propositional formula checker heerhugo","author":"Groote","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB30","series-title":"Proceedings of FMCAD, volume 1954 of LNCS","first-page":"354","article-title":"SAT-Based Image Computation with Application in Reachability Analisys","author":"Gupta","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB31","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF02430364","article-title":"Testing Heuristics: We Have It All Wrong","volume":"1","author":"Hooker","year":"1996","journal-title":"Journal of Heuristics"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB32","series-title":"Optimizing Tableaux Decision Procedures for Description Logics PhD thesis","author":"Horrocks","year":"1997"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB33","article-title":"On evaluating decision procedures for modal logic","author":"Hustadt","year":"1997","journal-title":"Proc. of IJCAI"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB34","first-page":"359","article-title":"Planning as satisfiability","author":"Kautz","year":"1992","journal-title":"Proc. of ECAI"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB35","article-title":"Blackbox: A new approach to the application of theorem proving to problem solving","author":"Kautz","year":"1998","journal-title":"Working notes of the Workshop on Planning as Combinatorial Search, held in conjunction with AIPS-98"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB36","series-title":"Heuristics Based on Unit Propagation for Satisfiability Problems. In Proc. of IJCAI","first-page":"366","author":"Li","year":"1997"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB37","series-title":"Integrating Equivalency Reasoning into Davis-Putnam Procedure. In Proc. of AAAI.","author":"Li","year":"2000"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB38","series-title":"Symbolic Model Checking: an Approach to the State Explosion Problem","author":"McMillan","year":"1993"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB39","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1018999721141","article-title":"Boosting complete techniques thanks to local search methods","volume":"22","author":"Mazure","year":"1998","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB40","article-title":"DLP System Description","author":"Patel-Schneider","year":"1998","journal-title":"Collected Papers from the International Description Logics Workshop (DL'98). CSEUR Workshop Proceedings"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB41","first-page":"1192","article-title":"Improvements to the Evaluation of Quantified Boolean Formulae","author":"Rintanen","year":"1999","journal-title":"Proc of IJCAI"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB42","unstructured":"ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB43","series-title":"GRASP - A new Search Algorithm for Satisfiability. Technical report","author":"Silva","year":"1996"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB44","author":"St\u00e5lmarck","year":"1994","journal-title":"System for Determining Prepositional Logic Theorems by Applying Values and Rules to Triplets that are Generated From Boolean Formula"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB45","article-title":"\u2217SAT system description","author":"Tacchella","year":"1999","journal-title":"Collected Papers from the International Description Logics Workshop (DL'99). CEUR Workshop Proceedings"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB46","article-title":"Search in a Small World","author":"Walsh","year":"1999","journal-title":"Proc. of the 16th International Joint Conference on Artificial Intelligence (IJCAI '99)"},{"key":"10.1016\/S1571-0653(04)00329-4_BIB47","series-title":"Highlights of Satisfiability Research in the Year 2000","article-title":"Implementing the Davis-Putnam Method","author":"Zhang","year":"2000"}],"container-title":["Electronic Notes in Discrete Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571065304003294?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571065304003294?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,27]],"date-time":"2019-01-27T08:50:23Z","timestamp":1548579023000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571065304003294"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,6]]},"references-count":47,"alternative-id":["S1571065304003294"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0653(04)00329-4","relation":{},"ISSN":["1571-0653"],"issn-type":[{"value":"1571-0653","type":"print"}],"subject":[],"published":{"date-parts":[[2001,6]]}}}