Number of the records: 1
A Lower Bound on CNF Encodings of the At-most-one Constraint
- 1.
SYSNO ASEP 0494392 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title A Lower Bound on CNF Encodings of the At-most-one Constraint Author(s) Kučera, P. (CZ)
Savický, Petr (UIVT-O) SAI, RID, ORCID
Vorel, V. (CZ)Source Title Theoretical Computer Science. - : Elsevier - ISSN 0304-3975
Roč. 762, March (2019), s. 51-73Number of pages 23 s. Language eng - English Country NL - Netherlands Keywords Knowledge compilation ; Cardinality constraint ; At most one constraint ; Propagation complete encoding Subject RIV IN - Informatics, Computer Science OECD category Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) R&D Projects GBP202/12/G061 GA ČR - Czech Science Foundation (CSF) Method of publishing Limited access Institutional support UIVT-O - RVO:67985807 UT WOS 000459528200005 EID SCOPUS 85053701165 DOI 10.1016/j.tcs.2018.09.003 Annotation Constraint 'at most one' is a basic cardinality constraint which requires that at most one of its n boolean inputs is set to 1. This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the 'at most one' constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related 'exactly one' constraint. Workplace Institute of Computer Science Contact Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Year of Publishing 2020 Electronic address http://dx.doi.org/10.1016/j.tcs.2018.09.003
Number of the records: 1