Diferencia entre revisiones de «Clase 2 (Especificación y Complejidad)»
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 | |||
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 | |||
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 | |||
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 del 20:10 26 feb 2009
Temas vistos en la clase
Reduccion de SAT a 3-SAT
Sea F = C1 ^ ... ^ Cn conjunción de clausulas
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
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
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