{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:50:00Z","timestamp":1748998200044},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Exotic semi-ring constraints arise in a variety of applications and<\/jats:p><jats:p>in particular in the context of automated termination analysis.<\/jats:p><jats:p>We propose two techniques to solve such constraints: (a) to model<\/jats:p><jats:p>them using Boolean functions and integer linear arithmetic and solve<\/jats:p><jats:p>them using an SMT solver (QF_LIA, in certain cases also QF_IDL);<\/jats:p><jats:p>and (b) to seek finite domain solutions by applying unary bit-blasting<\/jats:p><jats:p>and solve them using a SAT solver.<\/jats:p><jats:p>In this note, we show the structure of such systems of constraints,<\/jats:p><jats:p>and report on the performance of SMT solvers and SAT encodings when<\/jats:p><jats:p>solving them. In particular, we observe that good results are<\/jats:p><jats:p>obtained by unary bit-blasting, improving on previous proposals to<\/jats:p><jats:p>apply binary bit-blasting. Moreover, our results indicate that, for<\/jats:p><jats:p>our benchmarks, unary bit-blasting leads to better results than the<\/jats:p><jats:p>ones directly obtained by an SMT solver.<\/jats:p>","DOI":"10.29007\/qqvt","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:11Z","timestamp":1516730351000},"page":"88-77","source":"Crossref","is-referenced-by-count":5,"title":["Exotic Semi-Ring Constraints"],"prefix":"10.29007","volume":"20","author":[{"given":"Michael","family":"Codish","sequence":"first","affiliation":[]},{"given":"Yoav","family":"Fekete","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]},{"given":"Johannes","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"SMT 2012. 10th International Workshop on Satisfiability Modulo Theories"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:13Z","timestamp":1516730353000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/TXn"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/qqvt","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}