{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T16:17:52Z","timestamp":1774973872410,"version":"3.50.1"},"reference-count":12,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/tai.2003.1250177","type":"proceedings-article","created":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T21:26:50Z","timestamp":1078176410000},"page":"105-110","source":"Crossref","is-referenced-by-count":22,"title":["Probing-based preprocessing techniques for propositional satisfiability"],"prefix":"10.1109","author":[{"given":"I.","family":"Lynce","sequence":"first","affiliation":[]},{"given":"J.","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref4","article-title":"A simplifier for propositional formulas with many binary clauses","author":"brafman","year":"2001","journal-title":"IJCAI'01"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00314-2"},{"key":"ref10","first-page":"145","article-title":"Combinational equivalence checking using satisfiability and recursive learning","author":"marques-silva","year":"1999","journal-title":"Proc ACM\/IEEE Design Automation Test Eur Conf"},{"key":"ref6","article-title":"A backbone-search heuristic for efficient solving of hard 3-sat formulae","author":"dubois","year":"2001","journal-title":"IJCAI4"},{"key":"ref11","first-page":"185","article-title":"Recovering and exploiting structural knowledge from cnf formulas","author":"ostrowski","year":"2002","journal-title":"CP-02"},{"key":"ref5","article-title":"Experimental results on the crossover point in satisfiability problems","author":"crawford","year":"1993","journal-title":"AAAI-93"},{"key":"ref12","author":"st\u00e5lmarck","year":"1992","journal-title":"A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets That Are Generated from a Formula 1989"},{"key":"ref8","first-page":"291","article-title":"Integrating equivalency reasoning into davisputnam procedure","author":"li","year":"2000","journal-title":"AAAI-00"},{"key":"ref7","article-title":"Satisfiability testing with more reasoning and less guessing","author":"gelder","year":"1993","journal-title":"Second DIMACS Implementation Challenge"},{"key":"ref2","article-title":"Enhancing Davis Putnam with extended binary clause reasoning","author":"bacchus","year":"2002","journal-title":"AAAI'02"},{"key":"ref9","first-page":"341","article-title":"Look-ahead versus look-back for satisfiability problems","author":"li","year":"1997","journal-title":"CP'97"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90002-4"}],"event":{"name":"15th IEEE International Conference on Tools with Artificial Intelligence","location":"Sacramento, CA, USA","acronym":"TAI-03"},"container-title":["Proceedings. 15th IEEE International Conference on Tools with Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8840\/27974\/01250177.pdf?arnumber=1250177","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T15:50:30Z","timestamp":1489420230000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1250177\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1109\/tai.2003.1250177","relation":{},"subject":[]}}