Lògica a la informàtica

http://www.fib.upc.edu/fib/estudiar-enginyeria-informatica/assignatures.html?assig=LI

Roberto Nieuwenhuis <roberto@lsi.upc.edu>


“el que no mata engorda”        

“l’enciam no engorda”                

La conclusió lògica és que l’encian mata (si la primera premisa és certa).


P = {p, q, r}

Literal: p (literal positiu), ¬p (literal negatiu)

Clàusula:  - disjunció de literals (OR)

Cub:

CNF:

DNF:

Conversions:

Propietats:

Una DNF és satisfactible hi ha algun cub que no és de la forma .

Demostració:

 (amb )

CNF

DNF

SAT

Difícil

NP-Complet

Fàcil

Polinòmic (lineal)

Tautologia

Fàcil

Polinòmic (lineal)

Difícil

NP-Complet

Una CNF és tautologia  totes les clàusules són de la forma .

Si tenim una fórmula  sense cap format concret, volem trobar una  que sigui equisatisfactible ().

Mètode bèstia:

1) Moure ¬ cap a dins:

2)  (distributiva)

Problema: augmenta la mida de les formules de forma exponencial (i troba una formula equivalent quan amb una equisatisfactible en podriem tenir prou).

Transformació de Tseitin:

                

                        google docs

                

 (les clàusules de tots els nodes)

Resolució:

                

conjunt de clausules inicial

Acaba perquè només existeix un nombre finit de clàusules ().

        (closura sota resolució)

Demostració de la resolució:

Sigui I tal que

  1. Si I(p)=0, llavors com que  tenim que  i .
  2. Si I(p)=1, llavors anàlogament tenim que  i .

La resolució és correcte (tota clàusula  és conseqüència lògica d’, és a dir, ).

Una regla de deducció R és completa si mitjançant R podem deduïr totes les conseqüències lògiques, és a dir, per a tota fórmula F i conjunt de clàuses S, es compleix que  implica . La resolució no és completa.

Contraexemple que no és completa:

 però

Però sí que és refutacionalment completa (si S0 és insatisfactible, llavors trobarà la clàusula buida ). Demostracció:

Contrarecíproc: suposem que la clàusula buida no pertany a Res(S0). Veurem que llavors S0 és satisfactible. Sigui P={P1, …, Pn}, apliquem inducció sobre n:

Sigui , tenim . Per tant, . S’’ té 1 símbol menys ( no hi és). Per HI, S’’ és satisfactible.

Sigui I un model d’S’, “I ⊨ S’”, veurem que existeix un I0 (extensió d’I per a Pn) tal que I0 ⊨ S0. Hi ha dos casos:

En el primer cas, defineixo I0(Pn)=1 i per la resta I0 és com I, i tenim que I0 ⊨ S0.

Clàusula de Horn

És una clàusula amb com a màxim un literal positiu. Si una fòrmula composta per clàusules de Horn no té cap clàusula amb només un sol literal positiu (i cap negatiu), llavors és SAT (amb la interpretació on tot és fals).

Possibles clàusules:

  1. unitària positiva
  2. amb literal positiu però no unitària
  3. sense literal positiu però amb algun literal negatiu

Si hi ha algun cas 4, és insatisfactible. Si no hi ha cap clàusula de tipus 1 ni 4 és satisfactible (la interpretació “tot fals” és model).

ALGORISME... Mirar als apunts!

Clàusula de Krom

És una clàusula amb com a màxim dos literals. El problema 2-SAT és fàcil.

Dificultat del problema SAT segons el nombre de clàusules

Amb 0 clàuses, la probabilitat que un problema sigui satisfactible és 1; amb moltes clàuses, la probabilitat que sigui satisfactible és 0. I entre mig? Hi ha una phase transition prop d’una proporció clàusula/variable del 4.25.

Tècniques SAT

DPLL amb tres components que funcionen junts: learn, decide, forget.

Representem l’estat actual de la forma 1v¬2v3v4v5, on els literals vermells són decisions arbitràries i els literals que els segueixen venen determinats per aquests (unit propagation). Anomenem un literal vermell i els seus successors negres decision level.

Nota: problemes aleatoris i problemes industrials no tenen res a veure. Tècniques que són molt bones per a un tipus de problemes, poden ser inútils per a l’altre.

Implementació eficient de l’unit propagation


Vertex cover

Problema NP-complet. Donat un graf G=(V,E), podem escollir un subconjunt C de K elements de V tal que ?

Possible codificació:

Variables:

Clàusules:

Codificació alternativa:

Variables:

Clàusules:

Codificacions AMO (at most one)

Núm. variables auxiliars

Núm. clàusules

quadràtica

0

O(n2)

ladder

n

3n

Henle 3

n/2

3n

Henle 4

n/3

10/3 · n

log

logn

nlogn

A la pràctica va millor la Henle 4, segons experiència del professor.

Clàusules:

Un CSP (Constraint Solving Problem) està compost per:

SAT n’és un cas particular on tots els dominis són {0,1} i les restriccions són clàusules lògiques.

En un problema CSP amb restriccions complexes podem mirar de podar (pruning) el domini de les variables per eliminar-ne valors òbviament impossibles a partir de les restriccions. Un cop fet això el problema serà arc-consistent (= per cada valor di de cada Di hi ha alguna solució on xi=di).

En les codificacions AMO que hem vist, l’unit propagation preserva l’arc-consistència.

Cardinality constraints (“at most k”, x1+...+xn <= k)

Pseudo-boolean constraints (també 0-1 integer linear constraints)

Expressen restriccions de la forma a1x1+...+anxn <= k (per exemple, 3x1+4x2+5x3<=9).


Lògica de 1r ordre

Sintàxi

Termes: x, ,

Àtoms:

Formules: àtom, ,

Semàntica

I?

I ⊨ F

Anomenem àtom a un símbol de predicat aplicat a termes (símbols de funció i variables). Anomenem literal a un àtom o a un àtom negat.

Dir si una fórmula de primer ordre és satisfactible és un problema co-semi-decidibile (només està garantit que acabi si és insatisfactible). Podem fer-ho comprovant si □.

Dir si una fórmula de primer ordre és conseqüència lògica d’una altre, F⊨G, es pot provar amb , de manera que és semi-decidible.

Dir si una interpretacció satisfà una fórmula de primer ordre és indecidible en el cas que el domini sigui infinit (podem demostrar-ho amb una reducció al problema de resoldre polinomis) i exponencial en cas contrari.

Transformació a forma clausal:

  1. Moure les negacions cap a dins:
  1. Eliminar conflictes de nom.
  2. Moure els quantificadors cap endins (per millorar el punt 4).
  3. Skolemització (eliminar els quantificadors existencials):
  1. Moure els quantificadors universals al principi.
  2. Distributivitat.

Resolució

CvA                Dv¬B

---------------------------  si σ=mgu(A,B)                        mgu: most general unifier

        (CvD)σ

Exemple:

Q(x) v P(x,a)                R(y) v ¬P(b,y)

------------------------------------------------ σ={x=b, y=a}

        Q(b) v R(a)

Unificació (com trobar el mgu)

{f(...) = g(...)} u E                        → fallo si f != g        (f/g poden ser constants)

{f(s1, …, sn) = f(t1, …, tn)) u E        → {s1=t1, …, sn=tn) u E

{x=t} u E                                 → fallo si x apareix en t i x != t (occurs check)

{x=t} u E                                → {x=t} u E{x=t} si x apareix en E

(Podem veure que acaba per l’ordre lexicogràfic de (<num. variables no resoltes>, <num. símbols de predicat>); la 4a regla decrementa el nombre de variables -i pot incrementar el nombre de símbols de predicat- i la 2a regla només decrementa el nombre de símbols de predicat).