{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T05:25:39Z","timestamp":1740115539873,"version":"3.37.3"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"abstract":"<jats:p>In this paper we start an investigation to check the best we can do with SAT encodings for solving two important hard arithmetic problems, integer factorization and discrete logarithm. Given the current success of using SAT encodings for solving problems with linear arithmetic constraints, studying the suitability of SAT for solving non-linear arithmetic problems was a natural step. However, our results indicate that these two problems are extremely hard for state-of-the-art SAT solvers, so they are good benchmarks for the research community interested in finding good SAT encodings for practical constraints.<\/jats:p>","DOI":"10.3233\/978-1-60750-643-0-239","type":"book-chapter","created":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T12:06:08Z","timestamp":1740053168000},"source":"Crossref","is-referenced-by-count":0,"title":["Encoding Basic Arithmetic Operations for SAT-Solvers"],"prefix":"10.3233","author":[{"family":"B&eacute;jar Ram&oacute;n","sequence":"additional","affiliation":[]},{"family":"Fern&aacute;ndez C&egrave;sar","sequence":"additional","affiliation":[]},{"family":"Guitart Francesc","sequence":"additional","affiliation":[]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","Artificial Intelligence Research and Development"],"original-title":[],"deposited":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T12:27:06Z","timestamp":1740054426000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISSNISBN&issn=0922-6389&volume=220&spage=239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-60750-643-0-239","relation":{},"ISSN":["0922-6389"],"issn-type":[{"value":"0922-6389","type":"print"}],"subject":[],"published":{"date-parts":[[2010]]}}}