Test di soddisfacibilit`a per il calcolo proposizionaleunina.stidue.net/Universita' di...

'

&

$

%

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


'

&

$

%

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)


'

&

$

%

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ı )


'

&

$

%

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


'

&

$

%

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 ”


'

&

$

%

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


'

&

$

%

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 )


'

&

$

%

Fra poco:

Metodo di Davis-Putnam-Loveland-Logemann

( Martin D. Davis e stato allievo di Post e di Church )


'

&

$

%

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.


'

&

$

%

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 )

· · · · · · · · · · · ·


'

&

$

%

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}


'

&

$

%

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


'

&

$

%

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


'

&

$

%

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


'

&

$

%

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} , . . .}


'

&

$

%

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)


'

&

$

%

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 .


'

&

$

%

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). �


'

&

$

%

Per ricrearsi lo spirito:


Test di soddisfacibilit`a per il calcolo proposizionaleunina.stidue.net/Universita' di...

Documents

Transcript of Test di soddisfacibilit`a per il calcolo proposizionaleunina.stidue.net/Universita' di...