Misurare la difficoltà di istanze SAT

Question

Dato un esempio di SAT, vorrei essere in grado di stimare quanto sia difficile sarà quello di risolvere il caso.

Un modo è quello di eseguire risolutori esistenti, ma questo tipo di sconfitte lo scopo di stimare difficoltà. Un secondo modo potrebbe essere alla ricerca di un rapporto di clausole a variabili, come avviene per le transizioni di fase in random-SAT, ma sono sicuro che esistono metodi migliori.

Dato un esempio di SAT, ci sono alcune euristiche veloci per misurare la difficoltà? L'unica condizione è che queste euristiche essere più veloce di effettivamente in esecuzione risolutori SAT esistenti per l'istanza.

---

questione connessa

problemi

?? Quali SAT sono facili? su cstheory.SE. Questa domanda chiede sui set trattabili di istanze. Questa è una domanda simile, ma non esattamente la stessa cosa. Sono davvero interessato a un'euristica che data una singola istanza, fa una sorta di indovinare semi-intelligente se l'istanza sarà un difficile da risolvere.

Answer 1

In generale, questa è una domanda di ricerca molto pertinenti e interessanti. "Un modo è quello di eseguire risolutori esistenti ..." e quale sarebbe questo anche dirci esattamente? Abbiamo potuto vedere empiricamente che un'istanza sembra difficile per una specifica risolutore o di un algoritmo specifico / euristica, ma che cosa realmente raccontare la durezza dell'istanza?

Un modo che è stato perseguito è l'identificazione di varie proprietà strutturali dei casi che portano ad algoritmi efficienti. Queste proprietà sono infatti preferivano essere "facilmente" identificabili. Un esempio è la topologia del grafo vincolo sottostante, misurata utilizzando vari parametri width grafico. Per esempio è noto che un'istanza è risolvibile in tempo polinomiale se la treewidth del grafico vincolo sottostante viene limitata da una costante.

Un altro approccio è concentrata sul ruolo di struttura nascosta di istanze. Un esempio è il insieme backdoor , cioè l'insieme di variabili in modo tale che quando vengono istanziati, i restanti problema si semplifica in una classe trattabili. Ad esempio, Williams et al., 2003 [1] mostrano che anche se si tiene conto del costo di ricerca di variabili backdoor, si possono ancora ottenere un vantaggio computazionale complessiva concentrandosi su un set backdoor, purché l'insieme è sufficientemente piccolo. Inoltre, Dilkina et al., 2007 [2] Si noti che un risolutore chiamato Satz-Rand è notevolmente bravo a trovare piccoli backdoor forti su una serie di domini sperimentali.

Più recentemente, Ansotegui et al., 2008 [3] propongono l'uso dell'albero simile complessità spaziale come misura per risolutori DPLL-based. Essi dimostrano che lo spazio anche costante limitata implica l'esistenza di un algoritmo decisionale tempo polinomiale con lo spazio è il grado del polinomio (Teorema 6 nella carta). Inoltre, mostrano lo spazio è minore rispetto alla dimensione del ciclo-cutsets. Infatti, sotto certe ipotesi, lo spazio è minore della dimensione di backdoor.

Inoltre formalizzare quello che penso siete dopo, che è il seguente:

Trova una misura $ \ psi $, e un algoritmo che data una formula $ \ Gamma $ decide soddisfacibilità in tempo $ O (n ^ {\ psi (\ Gamma)}) $. Più piccola è la misura è, meglio caratterizza il durezza di una formula .

---

[1] Williams, Ryan, Carla P. Gomes, e Bart Selman. "Backdoors alle tipiche caso complessità". Conferenza internazionale comune sulla Intelligenza Artificiale. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes, e Ashish Sabharwal. "Compromessi nella complessità dei Backdoor Detection". Principi e pratica di Constraint Programming (CP 2007), pp. 256-270, 2007.

[3] Ansotegui, Carlos, Maria Luisa Bonet, Jordi Levy, e Felip Manya. "Misurare la durezza della SAT istanze." In Atti del Convegno Nazionale 23 su Intelligenza Artificiale (AAAI'08), pp. 222-228, 2008.

Answer 2

Poiché si sa circa la transizione di fase, mi permetta di citare alcuni altri controlli semplici di essere a conoscenza di (che sono probabilmente sussunto dall'analisi grafo dei vincoli):

• Alcuni generatori casuali SAT primi inavvertitamente creato formule per lo più facile perché hanno usato "densità costante", che significa una percentuale più o meno uguale di tutte le lunghezze clausola. Questi sono stati per lo più facile, perché 2-clausole e le unità semplificano notevolmente il problema, come ci si dovrebbe aspettare, e davvero lunghe clausole o non aggiungono molto ramificazione o facilitano iper-risoluzione ancora migliore. Così, sembra meglio attaccare con clausole di lunghezza fissa e vari altri parametri.
• Allo stesso modo, un potente regola semplificazione è puro letterale eliminazione. Ovviamente, una formula è davvero solo duro come il numero di letterali impuri esso contiene. Perché Risoluzione crea nuove clausole di numerazione $ | x | * | \ lnot x | $ (cioè, il prodotto di occorrenze di $ x $ e la sua negazione), il numero di risolventi viene massimizzata quando ci sono un numero uguale di letterali positivi e negativi per ciascuna variabile. Quindi, bilanciato SAT generatori.
• C'è anche una tecnica chiamata "No Triangolo SAT", che sembra essere piuttosto fresco [1], che è una sorta di generatore di hard-esempio che vieta "triangoli". Un triangolo è un insieme di clausole contenenti 3 variabili $ V_1, V_2, V_3 $ che si verificano a coppie in tutte le combinazioni in un certo insieme di clausole (ad esempio, $ \ {V_1, V_2, ... \}, \ {V_2, V_3, ... \}, \ {V_1, V_3, ... \} $ ). A quanto pare, triangoli tendono a rendere una formula facile per i solutori note.

[1] https://arxiv.org/pdf/1903.03592.pdf

Answer 3

In cima a risposta eccellente di Juho, ecco un altro approccio:

Ercsey-Ravasz & Toroczkai, durezza ottimizzazione come il caos transitorio in un approccio analogico al soddisfacimento di vincoli , volume di Nature Physics 7, pagine 966-970 (2011).

Questo approccio è quello di riscrivere il problema SAT in un sistema dinamico, in cui qualsiasi attrattore di il sistema è una soluzione al problema SAT. Bacini di attrazione del sistema sono più frattali come il problema diventa più difficile, e quindi la "difficoltà" dell'istanza SAT possono essere misurate esaminando come caotico i transitori sono prima converge sistema.

In pratica, questo significa partire un mazzo di solutori da diverse posizioni iniziali ed esaminando la velocità con cui risolutori sfuggono i transitori caotici prima di arrivare ad un attrattore.

Non è difficile a venire con un sistema dinamico per il quale le "soluzioni" sono soluzioni a un dato problema SAT, ma è un po 'più difficile per assicurarsi che le soluzioni sono tutte attrattori e non repellers. La loro soluzione è introdurre variabili di energia (simile a moltiplicatori di Lagrange) per rappresentare quanto male un vincolo è violato, e cercare di ottenere il sistema per ridurre al minimo l'energia del sistema.

È interessante notare che, usando il loro sistema dinamico, è possibile risolvere i problemi SAT in tempo polinomiale su un computer analogico, che di per sé è un risultato notevole. C'è un fermo; può richiedere in modo esponenziale di grandi tensioni per rappresentare le variabili energetiche, in modo purtroppo non si può realizzare questo su hardware fisico.