# A lower bound on CNF encodings of the at-most-one constraint

## TL;DR

This paper establishes a near-tight lower bound on the size of propagation complete CNF encodings for the at-most-one constraint, crucial for efficient problem translation in SAT solving.

## Contribution

It provides the first lower bound on clause size for propagation complete encodings of the at-most-one constraint, nearly matching existing best encodings.

## Key findings

- Lower bound nearly matches the size of known encodings
- Slightly improved lower bounds for 2-CNF encodings
- Bounds also apply to the exactly-one constraint

## Abstract

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.