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.^[1]

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.^[2] Anche l'estensione del problema per formule Horn quantificate può essere risolto in tempo polinomiale.^[3]

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.^[4][5]

Algoritmo

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

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 ${\displaystyle l}$ , quindi si esegue una propagazione unitaria (unit propagation): il letterale ${\displaystyle l}$  viene impostato a vero, tutte le clausole contenenti ${\displaystyle l}$  vengono rimosse e tutte le clausole contenenti ${\displaystyle \neg l}$  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

${\displaystyle (\neg a\lor \neg b\lor c)\,\land }$ 

${\displaystyle (\neg b\lor \neg c\lor d)\,\land }$ 

${\displaystyle (\neg f\lor \neg a\lor b)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (\neg e\lor f)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

${\displaystyle (\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

${\displaystyle (\neg a\lor \neg b\lor c)\,\land }$ 

${\displaystyle (\neg b\lor \neg c\lor f)\,\land }$ 

${\displaystyle (\neg f\lor b)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (f)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

${\displaystyle (\neg b\lor \neg c)}$ ,

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

${\displaystyle (\neg a\lor \neg b\lor c)\,\land }$ 

${\displaystyle (b)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

${\displaystyle (\neg b\lor \neg c)}$ .

Ora b dev'essere vero. La semplificazione restituisce:

${\displaystyle (\neg a\lor c)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

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

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

${\displaystyle a=false}$ ,

${\displaystyle b=true}$ ,

${\displaystyle c=false}$ ,

${\displaystyle d=false}$ ,

${\displaystyle e=false}$ ,

${\displaystyle f=true}$ .

Caso insoddisfacibile

Nella formula Horn

${\displaystyle (\neg a\lor \neg b\lor c)\,\land }$ 

${\displaystyle (\neg b\lor \neg c\lor f)\,\land }$ 

${\displaystyle (\neg f\lor b)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (f)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

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

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

${\displaystyle (\neg a\lor \neg b\lor c)\,\land }$ 

${\displaystyle (b)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

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

Ora b dev'essere vero, da cui abbiamo:

${\displaystyle (\neg a\lor c)\,\land }$ 

${\displaystyle (\neg e\lor \neg c\lor a)\,\land }$ 

${\displaystyle (\neg d\lor e)\,\land }$ 

${\displaystyle ()}$ .

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

Note

1. ^ (EN) Alfred Horn, On sentences which are true of direct unions of algebras, in Journal of Symbolic Logic, vol. 16, n. 1, marzo 1951, pp. 14-21, DOI:10.2307/2268661.
2. ^ (EN) Stephen Cook e Phuong Nguyen, Logical foundations of proof complexity, Cambridge University Press, 2010, p. 224, ISBN 978-0-521-51729-4. (Author's 2008 bozza, v. p.213f)
3. ^ (EN) H.K. Buning, Marek Karpinski e A. Flogel, Resolution for Quantified Boolean Formulas, in Information and Computation, vol. 117, n. 1, Elsevier, 1995, pp. 12-18, DOI:10.1006/inco.1995.1025.
4. ^ (EN) Reiner Hähnle, Advanced many-valued logics, in Dov M. Gabbay, Franz Günthner (a cura di), Handbook of philosophical logic, vol. 2, 2nd, Springer, 2001, p. 373, ISBN 978-0-7923-7126-7.
5. ^ (EN) Reiner Hähnle, Complexity of Many-valued Logics, in Melvin Fitting, Ewa Orłowska (a cura di), Beyond two: theory and applications of multiple-valued logic, Springer, 2003, ISBN 978-3-7908-1541-2.
6. ^ (EN) William F. Dowling e Jean H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, in Journal of Logic Programming, vol. 1, n. 3, 1984, pp. 267-284, DOI:10.1016/0743-1066(84)90014-1, MR 770156.

Bibliografia

• (EN) Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Marx Maarten, Joel Spencer, Moshe Y. Vardi, Yde Venema e Scott Weinstein, Finite model theory and its applications, Texts in Theoretical Computer Science. An EATCS Series, Berlin, Springer-Verlag, 2007, ISBN 978-3-540-00428-8, Zbl 1133.03001.

Voci correlate

• Propagazione unitaria
• Soddisfacibilità booleana
• 2-satisfiability

  Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica