Mostra el registre d'ítem simple
A parametric approach for smaller and better encodings of cardinality constraints
dc.contributor.author | Abío Roig, Ignasi |
dc.contributor.author | Nieuwenhuis, Robert Lukas Mario |
dc.contributor.author | Oliveras Llunell, Albert |
dc.contributor.author | Rodríguez Carbonell, Enric |
dc.contributor.other | Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics |
dc.date.accessioned | 2014-06-18T07:50:25Z |
dc.date.available | 2014-12-31T03:30:56Z |
dc.date.created | 2013 |
dc.date.issued | 2013 |
dc.identifier.citation | Abío, I. [et al.]. A parametric approach for smaller and better encodings of cardinality constraints. A: International Conference on Principles and Practice of Constraint Programming. "Principles and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings". Uppsala: Springer, 2013, p. 80-96. |
dc.identifier.isbn | 978-364240626-3 |
dc.identifier.uri | http://hdl.handle.net/2117/23251 |
dc.description.abstract | Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables can be true. They are crucial in many applications. Although sophisticated encodings for cardinality constraints exist, it is well known that for small n and k straightforward encodings without auxiliary variables sometimes behave better, and that the choice of the right trade-off between minimizing either the number of variables or the number of clauses is highly application-dependent. Here we build upon previous work on Cardinality Networks to get the best of several worlds: we develop an arc-consistent encoding that, by recursively decomposing the constraint into smaller ones, allows one to decide which encoding to apply to each sub-constraint. This process minimizes a function λ·num- vars + num-clauses, where λ is a parameter that can be tuned by the user. Our careful experimental evaluation shows that (e.g., for λ = 5) this new technique produces much smaller encodings in variables and clauses, and indeed strongly improves SAT solvers' performance. |
dc.format.extent | 17 p. |
dc.language.iso | eng |
dc.publisher | Springer |
dc.subject | Àrees temàtiques de la UPC::Informàtica::Programació |
dc.subject.lcsh | Constraint programming (Computer science) |
dc.title | A parametric approach for smaller and better encodings of cardinality constraints |
dc.type | Conference report |
dc.subject.lemac | Programació per restriccions (Informàtica) |
dc.contributor.group | Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
dc.identifier.doi | 10.1007/978-3-642-40627-0_9 |
dc.relation.publisherversion | http://link.springer.com/chapter/10.1007%2F978-3-642-40627-0_9 |
dc.rights.access | Open Access |
local.identifier.drac | 12881586 |
dc.description.version | Postprint (author’s final draft) |
local.citation.author | Abío, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. |
local.citation.contributor | International Conference on Principles and Practice of Constraint Programming |
local.citation.pubplace | Uppsala |
local.citation.publicationName | Principles and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings |
local.citation.startingPage | 80 |
local.citation.endingPage | 96 |