Come ottenere i valori 2-Sat

Question

Ogni volta che cercare un algoritmo per 2-Sat, torno l'algoritmo per la forma decisione del problema: esiste un insieme legale di valori che soddisfano tutte le clausole. Tuttavia, ciò non mi permette di trovare facilmente un insieme di valori booleani soddisfacenti.

Come posso efficientemente trovare una serie legale di valori in grado di soddisfare un'istanza 2-Sat?

Sto lavorando in C ++ con la libreria Boost e apprezzerei codice che può essere facilmente integrato.

Grazie in anticipo

Answer 1

Se si dispone di un algoritmo di decisione per rilevare se esiste un'assegnazione valida per 2-SAT, è possibile utilizzare che per trovare in realtà fuori l'assegnazione vera e propria.

Prima esecuzione algoritmo decisionale 2-SAT l'intera espressione. Si supponga che dice che c'è un incarico valido.

Ora, se x_1 è un letterale, Assegnare x_1 a 0. Ora calcolare il 2-SAT per l'espressione risultante (si dovrà assegnare altri letterali a causa di questo, per esempio se appare x_1 O x_3, è inoltre necessario impostare x_3 a 1).

Se l'expresion risultante è 2-soddisfacibile, allora si può prendere x_1 a 0, altrimenti prendere x_1 a 1.

Ora potete trovare questo fuori su ciascun letterale.

Per un algoritmo più efficiente, vorrei suggerire di provare a utilizzare l'approccio grafico di implicazione.

È possibile trovare maggiori informazioni qui: http://en.wikipedia.org/wiki/ 2-soddisfacibilità

La quota di competenza:

  

un'istanza 2-soddisfacibilità è   risolvibili se e solo se ogni variabile   dell'istanza appartiene a un diverso   fortemente connesso componente del   grafo delle implicazioni che la negazione   la stessa variabile. Dal momento che con forza   componenti collegati possono essere trovati in   tempo lineare da un algoritmo basato sulla   ricerca in profondità, la stessa lineari   tempo legato vale anche per   2-soddisfacibilità.

I letterali in ciascun componente fortemente connessa o sono tutti a zero o tutti 1.

Answer 2

C'è almeno un algoritmo che elenca tutte le soluzioni a un problema 2-sat, da Tomas Feder: http://www.springerlink.com/content/j582276p06276l12/