{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T07:32:01Z","timestamp":1723015921644},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,8]]},"abstract":"<jats:p>Array constraints are essential for handling data structures in automated reasoning and software verification. Unfortunately, the use of a typical finite domain (FD) solver based on local consistency-based filtering has strong limitations when constraints on indexes are combined with constraints on array elements and size. This paper proposes an efficient and complete FD-solving technique for extended constraints over (possibly unbounded) arrays. We describe a simple but particularly powerful transformation for building an equisatisfiable formula that can be efficiently solved using standard FD reasoning over arrays, even in the unbounded case. Experiments show that the proposed solver significantly outperforms FD solvers, and successfully competes with the best SMT-solvers.<\/jats:p>","DOI":"10.24963\/ijcai.2017\/171","type":"proceedings-article","created":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T05:14:07Z","timestamp":1501218847000},"page":"1231-1238","source":"Crossref","is-referenced-by-count":2,"title":["Efficient and Complete FD-solving for extended array constraints"],"prefix":"10.24963","author":[{"given":"Quentin","family":"Plazar","sequence":"first","affiliation":[{"name":"Inria Bretagne-Atlantique, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathieu","family":"Acher","sequence":"additional","affiliation":[{"name":"Inria Bretagne-Atlantique, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Bardin","sequence":"additional","affiliation":[{"name":"CEA, LIST, Gif-sur-Yvette, F-91191, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Gotlieb","sequence":"additional","affiliation":[{"name":"Simula Research Laboratory, Certus Center, Lysaker, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"number":"26","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)","University of Technology Sydney (UTS)","Australian Computer Society (ACS)"],"acronym":"IJCAI-2017","name":"Twenty-Sixth International Joint Conference on Artificial Intelligence","start":{"date-parts":[[2017,8,19]]},"theme":"Artificial Intelligence","location":"Melbourne, Australia","end":{"date-parts":[[2017,8,26]]}},"container-title":["Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T07:52:36Z","timestamp":1501228356000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2017\/171"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2017,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2017\/171","relation":{},"subject":[],"published":{"date-parts":[[2017,8]]}}}