# 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
    $(\neg a\lor \neg b\lor c)\,\land$
    $(\neg b\lor \neg c\lor d)\,\land$
    $(\neg f\lor \neg a\lor b)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(\neg e\lor f)\,\land$
    $(\neg d\lor e)\,\land$
    $(\neg b\lor \neg c)$,
ciascuna clausola ha un letterale negato. Quindi, impostando ogni variabile a falso tutte le formule saranno soddisfatte.

#### Caso soddisfacibile

Nella formula Horn
    $(\neg a\lor \neg b\lor c)\,\land$
    $(\neg b\lor \neg c\lor f)\,\land$
    $(\neg f\lor b)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(f)\,\land$
    $(\neg d\lor e)\,\land$
    $(\neg b\lor \neg c)$,
una clausola forza f ad essere vero, per cui impostiamo f a vero e semplifichiamo come segue:
    $(\neg a\lor \neg b\lor c)\,\land$
    $(b)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(\neg d\lor e)\,\land$
    $(\neg b\lor \neg c)$.
Ora b dev'essere vero. La semplificazione restituisce:
    $(\neg a\lor c)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(\neg d\lor e)\,\land$
    $(\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
    $(\neg a\lor \neg b\lor c)\,\land$
    $(\neg b\lor \neg c\lor f)\,\land$
    $(\neg f\lor b)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(f)\,\land$
    $(\neg d\lor e)\,\land$
    $(\neg b)$,
una clausola forza f ad essere vero, il che ci permette di semplificare come segue:
    $(\neg a\lor \neg b\lor c)\,\land$
    $(b)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(\neg d\lor e)\,\land$
    $(\neg b)$.
Ora b dev'essere vero, da cui abbiamo:
    $(\neg a\lor c)\,\land$
    $(\neg e\lor \neg c\lor a)\,\land$
    $(\neg d\lor e)\,\land$
Avendo ottenuto una clausola vuota, la formula iniziale è insoddisfacibile.