{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:05:11Z","timestamp":1725451511724},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Conflict-driven clause learning is currently the most efficient complete algorithm for satisfiability solving. However, a conflict-directed backtrack deletes potentially large portions of the current assignment that have no direct relation with the conflict. In this paper, we show that the CDCL algorithm can be generalized with a partial ordering on decision levels. This allows keeping levels that would otherwise be undone during backtracking under the usual total ordering. We implement partial ordering CDCL in a state-of-the-art CDCL solver and show that it significantly ameliorates satisfiability solving on some series of benchmarks.<\/jats:p>","DOI":"10.29007\/fblb","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:08Z","timestamp":1516730348000},"page":"124-108","source":"Crossref","is-referenced-by-count":0,"title":["CDCL with Less Destructive Backtracking through Partial Ordering"],"prefix":"10.29007","volume":"21","author":[{"given":"Anthony","family":"Monnet","sequence":"first","affiliation":[]},{"given":"Roger","family":"Villemaire","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:08Z","timestamp":1516730348000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/T45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/fblb","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}