Horn-soddisfacibilità

In logica, la Horn-soddisfacibilità (in inglese Horn-satisfiability, or HORNSAT) è il problema di decidere se una congiunzione di clausole di Horn proposizionali è soddisfacibile. Il problema, così come le clausole Horn, prende il nome da Alfred Horn.

Una clausola di Horn è una clausola con al più un letterale positivo e un qualunque numero di letterali negativi. Una formula Horn è una formula proposizionale in forma normale congiuntiva composta da clausole Horn.

Il problema HORNSAT è noto essere P-completo, ovvero rientra tra i problemi "più difficili" e "più espressivi" risolvibili in tempo polinomiale. Anche l'estensione del problema per formule Horn quantificate può essere risolto in tempo polinomiale.

Corrispettivi analoghi del problema di Horn-soddisfacibilità possono essere formulati anche per logiche proposizionali polivalenti. Gli algoritmi per risolvere questi problemi solitamente non sono lineari, ma alcuni di essi sono polinomiali.

Algoritmo

Il problema di Horn-soddisfabilità è risolvibile da un algoritmo di complessità temporale lineare.

Segue un esempio di algoritmo polinomiale che verifica la Horn-soddisfacibilità ricorsivo.

• Una prima condizione di terminazione è una formula in cui tutte le clausole attualmente esistenti contengono letterali negativi. In questo caso, tutte le variabili attualmente presenti nelle clausole possono essere impostate su false.
• Una seconda condizione di terminazione è una clausola vuota. In questo caso, la formula non ha soluzioni.
• Negli altri casi, la formula contiene una clausola unitaria positiva $l$, quindi si esegue una propagazione unitaria (unit propagation): il letterale $l$ viene impostato a vero, tutte le clausole contenenti $l$ vengono rimosse e tutte le clausole contenenti $negl$ vengono rimosse da questo letterale. Il risultato è una nuova formula di Horn, su cui possiamo reiterare l'algoritmo.

L'algoritmo di cui sopra permette di determinare l'eventuale assegnazione che rende vera la formula: tutte le variabili contenute in una clausola unitaria sono impostate al valore che soddisfa la clausola stessa; tutti gli altri letterali sono impostati a falso. L'assegnazioen risultante è il modello minimale della formula Horn, ovvero, l'assegnazione avente un insieme minimale (rispetto all'inclusione) di variabili vere.

Usando un algoritmo lineare per la propagazione unitaria, l'algoritmo è eseguito in tempo lineare rispetto alla dimensione della formula.

Esempi

Caso banale

Nella formula Horn

$(\mathrm{\neg }a\vee \mathrm{\neg }b\vee c)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c\vee d)\wedge$

$(\mathrm{\neg }f\vee \mathrm{\neg }a\vee b)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(\mathrm{\neg }e\vee f)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c)$,

ciascuna clausola ha un letterale negato. Quindi, impostando ogni variabile a falso tutte le formule saranno soddisfatte.

Caso soddisfacibile

Nella formula Horn

$(\mathrm{\neg }a\vee \mathrm{\neg }b\vee c)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c\vee f)\wedge$

$(\mathrm{\neg }f\vee b)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(f)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c)$,

una clausola forza f ad essere vero, per cui impostiamo f a vero e semplifichiamo come segue:

$(\mathrm{\neg }a\vee \mathrm{\neg }b\vee c)\wedge$

$(b)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c)$.

Ora b dev'essere vero. La semplificazione restituisce:

$(\mathrm{\neg }a\vee c)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }c)$.

Ci siamo così ricondotti ad un caso banale, per cui le variabili rimanenti possono essere tutte impostate a falso. L'assegnazione risultante è:

$a=false$,

$b=true$,

$c=false$,

$d=false$,

$e=false$,

$f=true$.

Caso insoddisfacibile

Nella formula Horn

$(\mathrm{\neg }a\vee \mathrm{\neg }b\vee c)\wedge$

$(\mathrm{\neg }b\vee \mathrm{\neg }c\vee f)\wedge$

$(\mathrm{\neg }f\vee b)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(f)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }b)$,

una clausola forza f ad essere vero, il che ci permette di semplificare come segue:

$(\mathrm{\neg }a\vee \mathrm{\neg }b\vee c)\wedge$

$(b)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$(\mathrm{\neg }b)$.

Ora b dev'essere vero, da cui abbiamo:

$(\mathrm{\neg }a\vee c)\wedge$

$(\mathrm{\neg }e\vee \mathrm{\neg }c\vee a)\wedge$

$(\mathrm{\neg }d\vee e)\wedge$

$()$.

Avendo ottenuto una clausola vuota, la formula iniziale è insoddisfacibile.

Bibliografia

• Template:Cita libro

Voci correlate

• Propagazione unitaria
• Soddisfacibilità booleana
• 2-satisfiability