{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:11Z","timestamp":1725495731858},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean variables. A popular idea to solve PB-constraints is to transform them to CNFs (via BDDs, adders and sorting networks [5, 11]) and process them using \u2013 increasingly improving \u2013 state-of-the-art SAT-solvers. Recent research have favored the approach that uses Binary Decision Diagrams (BDDs), which is evidenced by several new constructions and optimizations [2, 21]. We show that encodings based on comparator networks can still be very competitive. We present a system description of a PB-solver based on MiniSat+ [11] which we extended by adding a new construction of selection network called 4-Way Merge Selection Network, with a few optimizations based on other solvers. Experiments show that on many instances of popular benchmarks our technique outperforms other state-of-the-art PB-solvers.<\/jats:p>","DOI":"10.29007\/hh3v","type":"proceedings-article","created":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T19:16:15Z","timestamp":1552677375000},"page":"65-50","source":"Crossref","is-referenced-by-count":1,"title":["Competitive Sorter-based Encoding of PB-Constraints into SAT"],"prefix":"10.29007","volume":"59","author":[{"given":"Micha\u0142","family":"Karpi\u0144ski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Piotr\u00f3w","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"Proceedings of Pragmatics of SAT 2015 and 2018"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T19:16:16Z","timestamp":1552677376000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/tsHw"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/hh3v","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}