{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:28:29Z","timestamp":1725762509289},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Adding blocked clauses to a CNF formula can substantially speed up SAT-solving, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula [17, 19]. In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly for certain instance families when blocked clauses are added as a preprocessing step [10,22]. This fact is in contrast to, but not in contradiction with, prior results showing that Blocked- Clause Elimination (BCE) is sometimes an effective preprocessing step [14,15]. We suggest that the practical role of blocked clauses in SAT-solving might be richer than expected. Concretely, we propose a theoretical study of the complexity of Blocked-Clause Addition (BCA) as a preprocessing step for SAT-solving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might unblock a different clause that was previously blocked. This order-sensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of k-ary blocked clauses that can be added to an input formula F is NP-hard for every k \u2265 2.<\/jats:p>","DOI":"10.29007\/p5mc","type":"proceedings-article","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T22:10:10Z","timestamp":1716847810000},"page":"408-389","source":"Crossref","is-referenced-by-count":0,"title":["Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition"],"prefix":"10.29007","volume":"100","author":[{"given":"Bernardo","family":"Subercaseaux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T22:10:20Z","timestamp":1716847820000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/ZtQzZ"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/p5mc","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}