A cosa serve sabato e a cosa serve?

Question

Di recente ho visto un articolo di Reddit sull'uso di SAT per risolvere un puzzle [1]. Questo mi ha procurato molto curiosità su questa cosa "sat". Ho letto l'articolo di Wikipedia, ma vorrei chiedere a qualcuno di voi di spiegarmelo in termini più laici.

A cosa serve e a cosa serve? Può essere usato per attraversare una struttura dell'albero? Per analizzare i testi? Per la rottura della linea [2]? Per l'imballaggio bidone [3]? È una specie di tecnica di ottimizzazione?

Nella nota correlata, ho letto che NP vs P riguarda la scelta di quali numeri di una somma impostata su zero vs controllando se alcuni numeri si sommano a zero - è seduto in qualche modo correlato a questo?

[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/

[2] http://en.wikipedia.org/wiki/line_wrap

[3] http://en.wikipedia.org/wiki/bin_packing_problem

Answer 1

SAT è molto importante perché è NP-completo. Per capire cosa significa che hai bisogno di una chiara nozione di classi di complessità. Ecco un breve carrello:

• P è la classe di tutti i problemi che possono essere risolti nel tempo polinomiale (cioè veloce).

• NP è la classe di tutti i problemi per il quale una soluzione può essere verificata nel tempo polinomiale. Ciò significa che una determinata soluzione è veloce, ma trovarne una è di solito lenta (il tempo esponenziale spesso). A meno che il problema non sia nella parte P di NP ovviamente (come sottolineato di seguito P fa parte di NP, in quanto è possibile verificare facilmente).

Quindi c'è l'insieme di problemi NP-completi. Questo set contiene tutti i problemi così generici, puoi risolvere questi problemi anziché un altro da NP (questo si chiama riduzione di un problema su un altro). Ciò significa che puoi trasformare un problema da un dominio in un altro problema di completamento NP, fargli derivare una risposta e trasformare la risposta.

Spesso tuttavia si può dimostrare che un problema è completo NP, ma le trasformazioni non sono chiare per un altro dato problema.

SAT è così bello, perché è NP-completo, cioè puoi risolverlo invece di qualsiasi altro problema in NP e anche le riduzioni non sono così difficili da fare. TSP è un altro problema di completamento NP, ma le trasformazioni sono spesso molto più difficili.

Quindi, sì, SAT può essere usato per tutti questi problemi che stai menzionando. Spesso tuttavia questo non è fattibile. Dove è fattibile è, quando non si sa nessun altro algoritmo veloce, come il puzzle che menzioni. In questo caso non è necessario sviluppare un algoritmo per il puzzle, ma puoi utilizzare uno dei solisti SAT altamente ottimizzati là fuori e finirai con un ragionevole algoritmo veloce per il tuo puzzle.

Attraversare una struttura degli alberi è così semplice, ad esempio che qualsiasi trasformazione da e a SAT sarà molto probabilmente molto più complessa della semplice scrittura direttamente di attraversamento.

Answer 2

Per fare una lunga storia, un risolutore SAT è qualcosa a cui dai una formula booleana e ti dice se può trovare un valore per le diverse variabili in modo tale che la formula sia vera.

Esempio

supporre che a, b e c sono variabili booleane e vuoi sapere se a queste variabili può essere assegnato un valore che in qualche modo fa la formula (¬a ∨ b) ∧ (¬b ∨ c). Invia questa formula al solutore SAT e ti restituirà true. Anche i risolutori SAT spesso ti danno un incarico valido. In questo caso questo incarico potrebbe essere a: false, b:false, c:false.

A cosa può essere usato?

Non lo userei per attraversare alberi né per analizzare il testo o per rompere le linee. Tuttavia, è possibile usarlo quando si attraversa un albero per verificare se alcuni vincoli sull'albero sono soddisfatti. Puoi certamente usarlo per l'imballaggio del bidone, anche se alcuni solutori CSP specializzati probabilmente funzionano meglio su questo tipo di problemi.

I solutori SAT stanno diventando molto più comuni in questi giorni, specialmente in software come i pacchetti. Eclipse incorpora sat4j per gestire le dipendenze tra i suoi plugin. Altre applicazioni di SAT in genere includono il controllo del modello, le applicazioni di pianificazione, i configuratori, la pianificazione e molti altri.