{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T16:11:09Z","timestamp":1779379869307,"version":"3.53.1"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"abstract":"<jats:p>In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our approach aims at improving the filtering power of the original clauses while producing a small number of additional and relevant clauses. More precisely, an incomplete redundancy check is performed on each original clauses through unit propagation, leading to either a sub-clause or to a new relevant one generated by the clause learning scheme. This preprocessor is empirically compared to the best existing one in terms of size reduction and the ability to improve a state-of-the-art satisfiability solver.<\/jats:p>","DOI":"10.3233\/978-1-58603-891-5-525","type":"book-chapter","created":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:26:53Z","timestamp":1740133613000},"source":"Crossref","is-referenced-by-count":2,"title":["Vivifying Propositional Clausal Formulae"],"prefix":"10.3233","author":[{"family":"Piette C&eacute;dric","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Hamadi Youssef","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Sa&iuml;s Lakhdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","ECAI 2008"],"original-title":[],"deposited":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:06:10Z","timestamp":1740135970000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISSNISBN&issn=0922-6389&volume=178&spage=525"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-58603-891-5-525","relation":{},"ISSN":["0922-6389"],"issn-type":[{"value":"0922-6389","type":"print"}],"subject":[],"published":{"date-parts":[[2008]]}}}