{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T14:57:40Z","timestamp":1730213860434,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/date.2003.1253706","type":"proceedings-article","created":{"date-parts":[[2003,12,22]],"date-time":"2003-12-22T12:34:10Z","timestamp":1072096450000},"page":"810-815","source":"Crossref","is-referenced-by-count":11,"title":["Local search for Boolean relations on the basis of unit propagation"],"prefix":"10.1109","author":[{"given":"Y.","family":"Novikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","article-title":"Exploiting the real power of unit propagation look ahead","author":"berre","year":"0","journal-title":"Proc Workshop Theory and Applications of Satisfiability Testing"},{"journal-title":"CMU Benchmark Suite","year":"0","author":"velev","key":"17"},{"key":"18","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":"15","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"16","first-page":"23","volume":"13","author":"stalmarck","year":"2000","journal-title":"A Tutorial on Stalmarcks Proof Procedure for Propositional Logic\/\/Formal Methods in System Design"},{"journal-title":"Chaff Engineering An Efficient SAT Solver\/\/ Proceedings of DAC01 -2001","year":"0","author":"moskewicz","key":"13"},{"key":"14","first-page":"142","author":"goldberg","year":"0","journal-title":"Berk Min rfeti A Fast and Robust SATsolver\/\/ Proceedings of DATE02"},{"key":"11","article-title":"Improvements to propositional satisfiability search algorithms\/\/Ph D thesis","author":"freeman","year":"1995","journal-title":"Department of Computer and Information Science"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00126-5"},{"year":"0","key":"21"},{"key":"20","first-page":"537","article-title":"Algebraic simplification techniques for propositional satisfiability","author":"silva","year":"2000","journal-title":"International Conference on Principles and Practice of Constraint Programming"},{"year":"0","key":"22"},{"key":"23","article-title":"The interaction between simplification and search in propositional satisfiability","author":"lynce","year":"2001","journal-title":"CP01 Workshop on Modeling and Problem Formulation (Formal01"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.935509"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/43.310903"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/43.3140"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/43.536723"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"3","first-page":"14","author":"ben-sasson","year":"2000","journal-title":"Near Optimal Separation of Treelike and General Resolution\/\/ Proceedings of SAT-2000 Third Workshop on the Satisfiability Problem"},{"key":"2","first-page":"203","author":"bayardo","year":"1997","journal-title":"Using Csp Look-Back Techniques to Solve Real-World Sat Instances\/\/ Proceeding of the Fourteenth National Conference on Artificial Intelligence (Aaai97) Providence"},{"key":"10","article-title":"Boosting combinational search through randomization","author":"gomes","year":"1997","journal-title":"Proceedings of International Conference on Principles and Practice of Constraint Programming"},{"journal-title":"The Interplay of Randomization and Learning on Real-world Instances of Satisfiability\/\/Proceedings of AAAI Workshop on Leveraging Probability and Uncertainty in Computation","year":"2000","author":"baptista","key":"1"},{"key":"7","first-page":"394","volume":"5","author":"davis","year":"1962","journal-title":"A Machine Program for Theorem Proving\/\/Comminications of the"},{"year":"0","key":"30"},{"key":"6","first-page":"291","author":"li","year":"0","journal-title":"Integrating Equivalency Reasoning into Davis-Putnam Procedure\/\/ Proceedings of AAAI2000"},{"key":"5","first-page":"261","author":"groote","year":"2000","journal-title":"The Propositional Formula Checker HeerHugo\/\/SAT2000"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"9","first-page":"114","author":"goldberg","year":"0","journal-title":"Using Sat for Combinational Equivalence Checking\/\/ Proceedings of DATE01"},{"key":"8","first-page":"415","article-title":"Sat versus unsat\/\/johnson and trick second dimacs series in discrete mathematics and theoretical computer science","author":"dubois","year":"1996","journal-title":"American Mathematical Society"}],"event":{"name":"6th Design Automation and Test in Europe (DATE 03)","acronym":"DATE-03","location":"Munich, Germany"},"container-title":["2003 Design, Automation and Test in Europe Conference and Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8443\/26600\/01253706.pdf?arnumber=1253706","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T14:31:00Z","timestamp":1489415460000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1253706\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/date.2003.1253706","relation":{},"subject":[]}}