'
&
$
%
Test di soddisfacibilita per il
calcolo proposizionale
Eugenio G. Omodeo
Universita di Trieste
Dipartimento di Matematica e Informatica
TRIESTE a.a. 2010/11 16, 19 novembre 2010 1 of 19
'
&
$
%
Punti
• generalizzazioni del problema della soddisfacibilita
• il teorema di compattezza ( cenni )
• assurdita di dnf e tautologicita di cnf
• normalizzazione di enunciati in 3-cnf equisoddisfacibile
• insiemi di clausole di Horn e loro soddisfacimento
• verifica DPLL della soddisfacibilita di enunciati in cnf
TRIESTE a.a. 2010/11 16, 19 novembre 2010 2 of 19
'
&
$
%
Soddisfacibilita
1. Il problema di stabilire se un enunciato puo essere reso vero ( assegnando
opportuni valori f/v alle sue lettere ) · · ·
2. · · · puo essere esteso ad insiemi finiti ( interpretati come congiunzioni ) di
enunciati e perfino · · ·
3. ad insiemi infiniti
A rigore, il problema della soddisfacilita e del soddisfacimento sono problemi
distinti: per rispondere al primo, basta
• stabilire se un assegnamento tale da rendere vero l’enunciato esiste;
• per l’altro, occorre anche esibire un tale assegnamento
Il simultaneo soddisfacimento di infiniti enunciati puo richiedere la
determinazione dei valori di infinite lettere (non cosı la refutazione)
TRIESTE a.a. 2010/11 16, 19 novembre 2010 3 of 19
'
&
$
%
Soddisfacibilita: esempi
Quale/i assegnamento/i per soddisfare l’insieme
{ p0} ∪ { pi→ pi+1 : i = 0, 1, 2, . . . (ad infinitum) } ?
————
Supponiamo che in una popolazione, finita o infinita, di ragazzi e ragazze
ciascun ragazzo abbia un numero finito di amiche e che, per ogni intero k,
comunque si estraggano dalla popolazione k ragazzi maschi, il numero di
amiche che essi hanno, complessivamente, sia > k. E possibile sposare ciascun
ragazzo con una delle sue amiche, senza che nessun ragazzo o ragazza risulti
bigamo ?
( Il teorema di compattezza ci dira di sı )
TRIESTE a.a. 2010/11 16, 19 novembre 2010 4 of 19
'
&
$
%
Aspetti intriganti della soddisfacibilita
1. Come verificare se una cnf e soddisfacibile ?
2. Si puo stabilire se un insieme infinito di enunciati e ‘collettivamente’
soddisfacibile / assurdo ?
Il problema 1. e un famigerato problema NP-completo, ma un algoritmo
pratico fu proposto ( inizio anni 1960 ) da
Davis-Putnam-Loveland-Logemann
Il problema 2., insolubile—in generale—per via algoritmica, ha una parziale
risposta nel
Teorema di compattezza: Un insieme infinito di enunciati e assurdo solo se
ha sottoinsiemi finiti assurdi
TRIESTE a.a. 2010/11 16, 19 novembre 2010 5 of 19
'
&
$
%
Il teorema di compattezza e ‘costruttivo’ ?
• La via piu sbrigativa per dimostrare il teorema di compattezza passa
attraverso il ‘controverso’
lemma di Zorn
( equivalente all’assioma della scelta )
• Tuttavia e possibile arrivarci anche attraverso il non meno celebre
lemma di Konig :
“ Se un albero orientato ha infiniti nodi ma ogni nodo ha un
numero finito di discendenti immediati, allora dalla radice
dell’albero scaturisce almeno un percorso infinito ”
TRIESTE a.a. 2010/11 16, 19 novembre 2010 6 of 19
'
&
$
%
Due problemi banali
Si dice che un enunciato e in forma normale disgiuntiva ( in breve dnf ) se
esso e della forma D0∨D1∨ · · · ∨Dn, dove n > 0 e ciascun Di e f oppure e
una congiunzione Li,0 & · · · & Li,midi letterali Lij , con mi > 0, dove per
letterale si intende una lettera proposizionale o la negazione di una lettera
proposizionale. Si dice che un enunciato e in forma normale congiuntiva ( in
breve cnf ) se esso e della forma C0 & C1 & · · · & Cn, dove n > 0 e ciascun Ci
e v oppure e una disgiunzione Li,0∨ · · · ∨Li,mi, con mi > 0, di letterali Li,j
Un enunciato in dnf ( rispettivamente: in cnf ) e assurdo ( rispettivam.:
tautologico ) se e solo se ciascuno dei suoi disgiunti Di ( rispettivam.:
congiunti Ci ): o e f ( rispettivam.: v ), oppure contiene, simultaneamente,
una lettera Li,j1 e la sua negazione, Li,j1 = ¬ Li,j0
TRIESTE a.a. 2010/11 16, 19 novembre 2010 7 of 19
'
&
$
%
Svolta dei primi anni ’60: da dnf a cnf
Dag Prawitz, riducendo il problema della dimostrazione in logica predicativa
del prim’ordine a verifiche di assurdita di dnf, si scontro con difficolta
insormontabili nella ricerca automatica di dimostrazioni modeste
Riuscirono a andare molto piu lontano Martin Davis e Hilary Putnam
riportandosi a verifiche di assurdita di cnf
D&P contribuirono alla scoperta di due algoritmi fondamentali della logica
computazionale:
• test di soddisfacibilita per cnf,
• unificazione per il calcolo predicativo del 1.o ordine
( il secondo in realta gia scoperto da Jacques Herbrand nel 1930, anche se
popolarmente attribuito ad Alan Robinson, 1965 )
TRIESTE a.a. 2010/11 16, 19 novembre 2010 8 of 19
'
&
$
%
Fra poco:
Metodo di Davis-Putnam-Loveland-Logemann
( Martin D. Davis e stato allievo di Post e di Church )
TRIESTE a.a. 2010/11 16, 19 novembre 2010 9 of 19
'
&
$
%
3-cnf equisoddisfacibile - I
Teorema. Ogni enunciato E e equi-soddisfacibile con un enunciato C in cnf,
la cui lunghezza e linearmente correlata alla lunghezza di E e nel quale nessun
congiunto contiene piu di tre letterali.
Idea. Si visiti l’enunciato ( rappresentato come albero di sintassi )
• procedendo dalle foglie verso la radice,
• associando un nuovo temporaneo a rappresentare ciascun nodo interno,
• correlando ciascun temporaneo ai suoi operandi secondo la tabella di
conversione del prossimo lucido, e
• applicando via via la legge di doppia negazione.
Il temporaneo che rappresenta l’intero enunciato venga aggiunto alla fine come
congiunto a se.
TRIESTE a.a. 2010/11 16, 19 novembre 2010 10 of 19
'
&
$
%
3-cnf equisoddisfacibile - II
Z ↔X & Y ( Z→X ) & ( Z→Y ) & ( X & Y →Z )
(¬Z∨X ) & (¬Z∨Y ) & (¬X∨¬Y ∨Z )
Z↔X ∨ Y ( X→Z ) & (Y→Z ) & ( Z→X∨Y )
(¬X∨Z ) & (¬Y ∨Z ) & (¬Z∨X∨Y )
Z↔( X↔Y ) ( Z & X→Y ) & ( Z & Y→X )
& ( X & Y →Z ) & ( ¬X & ¬Y →Z )
(¬Z∨¬X∨Y ) & (¬Z∨¬Y ∨X )
& (¬X∨¬Y ∨Z ) & ( X∨Y ∨Z )
· · · · · · · · · · · ·
TRIESTE a.a. 2010/11 16, 19 novembre 2010 11 of 19
'
&
$
%
Da cnf ad insiemi di clausole - I
L’operazione di complementazione
L 7→ L
agisce mettendo o togliendo ( a seconda che ci sia o che manchi ), all’inizio, il
simbolo di negazione. A noi basta complementare i letterali:
• quando ` e una lettera proposizionale, allora
• ` e ¬`
• ¬` e `
Questa operazione gode delle proprieta di una connessione di Galois:
• L 6= L
• L = L
Rappresentare la complementazione come inversione di segno in Z \ {0}
TRIESTE a.a. 2010/11 16, 19 novembre 2010 12 of 19
'
&
$
%
Da cnf ad insiemi di clausole - II
Le operazioni di disg-/cong-iunzione godono delle proprieta di
commutativita: E∨F = F∨E , E & F = F & E
assorbimento: E∨E = E , E & E = E
Percio Davis & Putnam proposero di codificare le
disgiunzioni come insiemi, detti clausole, di interi non-nulli
congiunzioni come insiemi di clausole
( La rappresentazione delle clausole come insiemi venne originariamente
realizzata, ai Bell Labs, tramite numeri in rappresentazione ternaria )
A margine:
C1∨ · · · ∨Cn∨¬A1∨ · · · ∨¬Am = C1∨ · · · ∨Cn← A1 & · · · & Am
TRIESTE a.a. 2010/11 16, 19 novembre 2010 13 of 19
'
&
$
%
Clausole di Horn
Una disgiunzione `1∨ · · · ∨`M di letterali dei quali al piu uno e affermativo si
chiama clausola di Horn
Puo essere ( per ora ) un
fatto: ossia una lettera proposizionale H
regola: ossia una lettera H accompagnata da letterali negativi, dunque
riscrivibile come:
H ← A0 & · · · & AM−2 , ove le Ai sono lettere
goal: solo letterali negativi, dunque
¬A1∨ · · · ∨¬AM
TRIESTE a.a. 2010/11 16, 19 novembre 2010 14 of 19
'
&
$
%
Soddisfacimento di clausole di Horn
In assenza di goal, la soddisfacibilita di una congiunzione di clausole di Horn
e assicurata: c’e un ‘modello minimo’, nel senso che assegna v a una lettera
solo se tale valore e obbligato
Metodo di concatenamento in avanti: Si parte dall’acquisire i fatti, dei quali
si eliminano i complementi nelle altre clausole, fin quando non si liberano piu
fatti nuovi
Se ci sono anche goal, una volta individuato il modello minimo, ci si
domanda se qualche goal non si sia per caso ‘svuotato’, nel qual caso la
congiunzione e assurda
TRIESTE a.a. 2010/11 16, 19 novembre 2010 15 of 19
'
&
$
%
Esempio - I
Si considerino le clausole:
a
b
c← b
c←m & e
g←m & e & c
m← a & b & c
f ← b & g
f ←m & h
f ← b & m
ovvero, secondo la rappresentazione delle clausole introdotta da Davis-Putnam:
{{1}, {2}, {−2, 3}, {−4,−5, 3}, {−4,−5,−3, 7}, {−2,−7}, {−4,−6}, {−2,−4},{4,−1,−2,−3} , . . .}
TRIESTE a.a. 2010/11 16, 19 novembre 2010 16 of 19
'
&
$
%
Esempio - II
A seconda che si includa o meno la regola su m, i goal saranno tutti o tre
soddisfacibili, o soddisfacibili i primi due ma non il terzo.
Queste prove si possono effettuare anche nel linguaggio di programmazione
Prolog, dove pero la ricerca dell’assurdo procede per concatenamento a
ritroso, che puo causare ( perfino a livello proposizionale ) un
‘impantanamento’ (in inglese: floundering)
TRIESTE a.a. 2010/11 16, 19 novembre 2010 17 of 19
'
&
$
%
Algoritmo DPLL - I
Ecco i criteri di Davis-Putnam:
1) Un enunciato in cnf e manifestamente soddisfacibile quando ha la forma
v & · · · & v.
2) Un enunciato in cnf e manifestamente insoddisfacibile quando gli
appartengono due clausole mono-letterali, una complemento dell’altra.
3) La seguente semplificazione non influisce sulla soddisfacibilita (o
insoddisfacibilita) di un enunciato in cnf : rimpiazzare con v una clausola
Ci quando il complemento di uno dei suoi letterali Lih
• e anch’esso letterale Lik di Ci, oppure
• non e letterale Ljk di nessun’altra clausola Cj .
TRIESTE a.a. 2010/11 16, 19 novembre 2010 18 of 19
'
&
$
%
Algoritmo DPLL - II
4) La seguente semplificazione non influisce sulla soddisfacibilita di un un
enunciato in cnf : quando una clausola Ci e formata dal solo letterale Li0,
ed il complemento di Li0 non e una clausola, rimpiazzare con v tutte le
clausole cui appartiene Li0 (in particolare Ci), cancellare poi il
complemento di Li0 da tutte le clausole Cj di cui esso e un Ljk.
5) Quando un enunciato in cnf non puo essere risolto o semplificato
utilizzando uno dei precedenti criteri 1)–4), allora puo venire scisso in due
enunciati in cnf tali che l’enunciato di partenza e soddisfacibile se e solo
se almeno uno dei due nuovi e soddisfacibile. La scissione si effettua
utilizzando un letterale Lij scelto ad arbitrio, semplicemente inserendo
una nuova clausola: in un caso Lij , nell’altro il complemento di Lij .
Si noti che per il trattamento di entrambi gli enunciati che risultano dalla
scissione, si potra subito ricorrere a 2) o a 4). �
TRIESTE a.a. 2010/11 16, 19 novembre 2010 19 of 19
'
&
$
%
Per ricrearsi lo spirito:
TRIESTE a.a. 2010/11 16, 19 novembre 2010 20 of 19
Top Related