Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/14739

BDDs for Pseudo-Boolean Constraints
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Universitat Politècnica de Catalunya. Departament de Matemàtica Aplicada I; Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
Pseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings are based on building Binary Decision Diagrams (BDDs) and translating these into CNF. Indeed, BDD-based encodings have important advantages, such as sharing the same BDD for representing many constraints. Here we first prove that, unless NP = Co-NP, there are Pseudo- Boolean constraints that admit no variable ordering giving a polynomial (Reduced, Ordered) BDD. As far as we know, this result is new (in spite of some misleading information in the literature). It gives several interesting insights, also relating proof complexity and BDDs. But, more interestingly for practice, here we also show how to overcome this theoretical limitation by coefficient decomposition. This allows us to give the first polynomial arc-consistent BDD-based encoding for Pseudo-Boolean constraints.
Peer Reviewed
Àrees temàtiques de la UPC::Informàtica
Lògica matemàtica
Algorismes -- Informàtica
Attribution-NonCommercial-NoDerivs 3.0 Spain
http://creativecommons.org/licenses/by-nc-nd/3.0/es/
info:eu-repo/semantics/publishedVersion
info:eu-repo/semantics/conferenceObject
Springer Verlag
         

Mostrar el registro completo del ítem

Documentos relacionados

Otros documentos del mismo autor/a

Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter
Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Abío Roig, Ignasi; Deters, Morgan; Nieuwenhuis, Robert Lukas Mario; Stuckey, Peter
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto