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. (Author's 2008 bozza, v. p.213f) 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 , quindi si esegue una propagazione unitaria (unit propagation): il letterale viene impostato a vero, tutte le clausole contenenti vengono rimosse e tutte le clausole contenenti 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'assegnazione 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
, ciascuna clausola ha un letterale negato. Quindi, impostando ogni variabile a falso tutte le formule saranno soddisfatte.
Caso soddisfacibile Nella formula Horn
,
una clausola forza f ad essere vero, per cui impostiamo f a vero e semplifichiamo come segue:
.
Ora b dev'essere vero. La semplificazione restituisce:
.
Ci siamo così ricondotti ad un caso banale, per cui le variabili rimanenti possono essere tutte impostate a falso. L'assegnazione risultante è: , , , , , .
Caso insoddisfacibile Nella formula Horn
,
una clausola forza f ad essere vero, il che ci permette di semplificare come segue:
.
Ora b dev'essere vero, da cui abbiamo:
. Avendo ottenuto una clausola vuota, la formula iniziale è insoddisfacibile.
Note
Bibliografia
Voci correlate Propagazione unitaria Soddisfacibilità booleana 2-satisfiability
Categoria:Soddisfacibilità booleana Categoria:Logica nell'informatica