Diferencia entre revisiones de «Clase 2 (Especificación y Complejidad)»

De Cuba-Wiki
 
 
(No se muestra una edición intermedia del mismo usuario)
Línea 2: Línea 2:


=Temas vistos en la clase=
=Temas vistos en la clase=
==Reduccion de SAT a 3-SAT==
Sea F = C1 ^ ... ^ Cn  conjunción de clausulas  (^ operador And)
Sea µi(Ci)= # literales de Ci
 
Sea µ(F) = max{µi(Ci)}
Si pasa que µ(F)> 3 , reemplazamos F por F' con µ(F') < µ(F) en un procedimiento recursivo
Sea x nueva variable booleana y sin restriccion de generalidad µ(F)=µ1(C1)
Entonces C1 = l1 v ... v ls con s>3  (li es un literal, v operador Or)
Defino
C1'  = l1 v l2 v x
C1' ' = l3 v ... v ls v ¬x
Observacion: F es satisfacible sii F'= C1' ^ C1' ' ^ C2 ^ ... ^ Cn  es satisfacible
Demo:
sea valuacion V , tal que V(F)=1
Entonces en particular V(C1)=1 , mas especificamente V(l1 v l2)=1 ó V(l3 v ... v ls)=1
Luego hay dos casos:
Si V(l1 v l2)=1 entonces defino V(x)=0
Sino, Si V(l3 v ... v ls)=1 entonces defino V(x)=1
Lo puedo hacer porque x es nueva y no afecta V(F)
En ambos casos vale V(C1')= V(C1' ')= 1, mantenemos satisfabilidad.
Y vale que µ(F')= µ(F)-1      ■
Para completar habria que demostrar que la longitud maxima de la clausula de F se baja a 3
en tiempo polinomial.
Segun Joos es O(│F│^2)


=Bibliografía recomendada para esta clase=
=Bibliografía recomendada para esta clase=

Revisión actual - 20:30 26 feb 2009

Plantilla:Back

Temas vistos en la clase

Reduccion de SAT a 3-SAT

Sea F = C1 ^ ... ^ Cn conjunción de clausulas (^ operador And)

Sea µi(Ci)= # literales de Ci

Sea µ(F) = max{µi(Ci)}

Si pasa que µ(F)> 3 , reemplazamos F por F' con µ(F') < µ(F) en un procedimiento recursivo


Sea x nueva variable booleana y sin restriccion de generalidad µ(F)=µ1(C1)

Entonces C1 = l1 v ... v ls con s>3 (li es un literal, v operador Or)

Defino

C1'  = l1 v l2 v x
C1' ' = l3 v ... v ls v ¬x


Observacion: F es satisfacible sii F'= C1' ^ C1' ' ^ C2 ^ ... ^ Cn es satisfacible

Demo: sea valuacion V , tal que V(F)=1

Entonces en particular V(C1)=1 , mas especificamente V(l1 v l2)=1 ó V(l3 v ... v ls)=1

Luego hay dos casos:

Si V(l1 v l2)=1 entonces defino V(x)=0

Sino, Si V(l3 v ... v ls)=1 entonces defino V(x)=1

Lo puedo hacer porque x es nueva y no afecta V(F)

En ambos casos vale V(C1')= V(C1' ')= 1, mantenemos satisfabilidad.

Y vale que µ(F')= µ(F)-1 ■


Para completar habria que demostrar que la longitud maxima de la clausula de F se baja a 3 en tiempo polinomial.

Segun Joos es O(│F│^2)

Bibliografía recomendada para esta clase

http://www.academic.marist.edu/~jzbv/algorithms/3SAT.htm

Links externos de esta sección