{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T07:59:01Z","timestamp":1791100741753,"version":"4.1.0"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>One of the design principles of the state-of-the-art SAT solver Lingeling is to use as compact data structures as possible. These reduce memory usage, increase cache efficiency and thus improve run-time, particularly, when using multiple solver instances on multi-core machines, as in our parallel portfolio solver Plingeling and our cube and conquer solver Treengeling. The scheduler of a dozen inprocessing algorithms is an important aspect of Lingeling as well. In this talk we explain these design and implementation aspects of Lingeling and discuss new direction of solver design.<\/jats:p>","DOI":"10.29007\/jhd7","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:59Z","timestamp":1516730579000},"page":"88-86","source":"Crossref","is-referenced-by-count":11,"title":["Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling"],"prefix":"10.29007","volume":"27","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"11545","event":{"name":"POS-14. Fifth Pragmatics of SAT workshop"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:59Z","timestamp":1516730579000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/xJs"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/jhd7","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}