Near-Optimal Encodings of Cardinality Constraints

1. Il Problema

I vincoli di cardinalità sono fondamentali nella teoria della soddisfacibilità booleana (SAT) per codificare problemi in forma normale congiuntiva (CNF). In particolare, il vincolo AtMostOne ($AtMostOne(x_1, \dots, x_n)$) afferma che al massimo una variabile booleana tra $n$ è vera.

• Sfida principale: Una codifica diretta richiede $\binom{n}{2}$ clausole (crescita quadratica), il che è inefficiente per $n$ grandi.
• Stato dell'arte: Esistono codifiche lineari $O(n)$ che introducono variabili ausiliarie. Prima di questo lavoro, la codifica più efficiente nota era la "product encoding" di Chen (2010), che utilizzava $2n + 4\sqrt{n} + O(\sqrt[4]{n})$ clausole ed era considerata ottimale secondo una congettura.
• Domande aperte:
  1. La congettura di Chen sull'ottimalità della product encoding è vera?
  2. Esiste un limite inferiore non banale per le codifiche di AtMostOne senza assumere la "completezza di propagazione"?
  3. Come si possono migliorare le codifiche per AtMostk (al massimo $k$ variabili vere) quando $k$ è piccolo rispetto a $n$?

2. Metodologia e Nuove Tecniche

Gli autori introducono tre tecniche principali per costruire codifiche più compatte:

A. Riformulazione Grafica e Codifica Multipartita (per AtMostOne)

• Nuova prospettiva: Gli autori reinterpretano la product encoding di Chen non come una griglia, ma come un grafo bipartito completo. In questa visione, le variabili di input sono gli archi e le variabili ausiliarie sono i vertici.
• Innovazione: Invece di un grafo bipartito, utilizzano un grafo multipartito completo con $\omega(1)$ parti. Questo permette di aumentare la densità degli archi (da $1/2$ a $1$), riducendo il numero di vertici (variabili ausiliarie) necessari per lo stesso numero di archi (variabili di input).
• Struttura: La codifica introduce un vincolo AtMost2 all'interno della sua definizione, rendendo la codifica finale in 3-CNF (anche se AtMostOne è una funzione 2-CNF). Questo contraddice l'ipotesi comune che le codifiche ottimali debbano essere 2-CNF.

B. Disjunctive Switching (Interruzione Disgiuntiva)

• Concetto: Una tecnica ispirata alla gestione dei "switch" negli algoritmi. Invece di codificare esplicitamente tutti i rami possibili di una condizione (che porta a una somma di dimensioni), si usano clausole ampie (wide clauses) per affermare che uno dei rami sarà preso, e si vincola l'attivazione dei rami non presi.
• Applicazione: Permette di ridurre le clausole di proiezione nella codifica generalizzata del prodotto. Ad esempio, invece di $k+1$ implicazioni per variabile, se ne usano solo 2, spostando la complessità su vincoli di controllo più efficienti.

C. Grid Compression (Compressione a Griglia)

• Ispirazione: Ispirata alle tabelle hash.
• Meccanismo: Le variabili di input vengono disposte in una griglia $M$. Questa griglia viene "compressa" in una griglia più piccola $L$ mappando le colonne occupate di $M$ su colonne di $L$.
• Vantaggio: Si impone il vincolo AtMostk sulla griglia più piccola $L$, che richiede meno risorse. La mappatura utilizza proprietà combinatorie (famiglie di insiemi cover-free o teorema di Hall) per garantire che la compressione sia invertibile e corretta.

3. Contributi Chiave e Risultati Teorici

Per AtMostOne

1. Smentita della Congettura di Chen: Gli autori presentano una codifica (Multipartite Encoding) che utilizza $2n + 2\sqrt{2n} + O(\sqrt[3]{n})$ clausole. Questo è strettamente migliore della product encoding di Chen ($2n + 4\sqrt{n}$), smentendo la sua presunta ottimalità.
2. Nuovo Limite Inferiore: Viene provato il primo limite inferiore incondizionato (senza assumere la completezza di propagazione) per AtMostOne: ogni codifica richiede almeno $2n + \sqrt{n} + 1 - 2$ clausole. Questo risponde a una domanda aperta di Kučera, Savický e Vorel.
3. Impatto sulla Complessità dei Circuiti: La costruzione fornisce un circuito booleano monotono più piccolo per la funzione soglia-2 (negazione di AtMostOne), migliorando un risultato di Adleman di 50 anni fa. Questo risolve un problema aperto di 47 anni sulla "congettura del singolo livello" (single-level conjecture), dimostrando che i circuiti ottimali per questa funzione non sono a singolo livello.

Per AtMostk

1. Codifiche più piccole per $k$ piccolo:
   • Grid Compression (Teorema 3): Codifica con $4n + o(n)$ clausole per $k = o(n)$.
   • Disjunctive Grid Compression (Teorema 4): Utilizzando la tecnica di "disjunctive switching", si ottiene una codifica con $2n + o(n)$ clausole per $k = o(\sqrt[3]{n})$.
2. Generalizzazione del Prodotto Disgiuntivo (Teorema 7): Viene mostrata come la codifica generalizzata del prodotto possa essere "disgiuntivizzata" per ottenere $2n + O(k n^{k/(k+1)})$ clausole, superando i limiti precedenti di $(k+1)n$.

4. Valutazione Empirica

Gli autori hanno testato le nuove codifiche (in particolare la Disjunctive Grid Compression - DGC) su diversi benchmark:

• Risultati: Sebbene le nuove codifiche non siano "propagation complete" (una proprietà spesso considerata essenziale per le prestazioni dei solver SAT), in molti casi pratici (specialmente per istanze facili o di grandi dimensioni) le prestazioni sono competitive o superiori rispetto alle codifiche classiche come il "sequential counter".
• Implicazione: I risultati mettono in discussione la saggezza convenzionale secondo cui la completezza di propagazione è assolutamente necessaria per ottenere buone prestazioni pratiche, suggerendo che il numero ridotto di clausole può compensare la mancanza di tale proprietà in certi contesti.

5. Significato e Impatto

• Teorico: Il lavoro risolve problemi aperti di lunga data nella teoria della complessità dei circuiti e nella teoria delle codifiche CNF, fornendo limiti superiori e inferiori quasi ottimali.
• Pratico: Introduce nuove tecniche (Grid Compression, Disjunctive Switching) che possono essere applicate ad altri problemi di codifica booleana.
• Paradigma: Dimostra che l'uso di clausole di larghezza maggiore (3-CNF) e tecniche non tradizionali possono portare a codifiche più efficienti, aprendo nuove direzioni di ricerca per l'ottimizzazione dei solver SAT.

In sintesi, il paper ridefinisce i limiti teorici della compressione dei vincoli di cardinalità e offre strumenti pratici che sfidano le assunzioni consolidate nel campo della soddisfacibilità booleana.