Mostra el registre d'ítem simple

dc.contributor.authorAbío Roig, Ignasi
dc.contributor.authorNieuwenhuis, Robert Lukas Mario
dc.contributor.authorOliveras Llunell, Albert
dc.contributor.authorRodríguez Carbonell, Enric
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
dc.date.accessioned2014-06-18T07:50:25Z
dc.date.available2014-12-31T03:30:56Z
dc.date.created2013
dc.date.issued2013
dc.identifier.citationAbí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.isbn978-364240626-3
dc.identifier.urihttp://hdl.handle.net/2117/23251
dc.description.abstractAdequate 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.extent17 p.
dc.language.isoeng
dc.publisherSpringer
dc.subjectÀrees temàtiques de la UPC::Informàtica::Programació
dc.subject.lcshConstraint programming (Computer science)
dc.titleA parametric approach for smaller and better encodings of cardinality constraints
dc.typeConference report
dc.subject.lemacProgramació per restriccions (Informàtica)
dc.contributor.groupUniversitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
dc.identifier.doi10.1007/978-3-642-40627-0_9
dc.relation.publisherversionhttp://link.springer.com/chapter/10.1007%2F978-3-642-40627-0_9
dc.rights.accessOpen Access
local.identifier.drac12881586
dc.description.versionPostprint (author’s final draft)
local.citation.authorAbío, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.
local.citation.contributorInternational Conference on Principles and Practice of Constraint Programming
local.citation.pubplaceUppsala
local.citation.publicationNamePrinciples and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings
local.citation.startingPage80
local.citation.endingPage96


Fitxers d'aquest items

Thumbnail

Aquest ítem apareix a les col·leccions següents

Mostra el registre d'ítem simple