[Tarea 4] Formato input e implicancias en CNF

[ljrodriguez1]

Hola escribo para saber como será el input de la tarea,

yo estoy asumiendo que será un archivo con una lineal, que será una gran formula en CNF. como la del enunciado.

O podrá ser que este archivo tiene varias líneas con varias formulas en CNF.

Por otro lado no logro imaginarme como se ve una implicancia en CNF. será de la forma:

(x1 -> (x2 0 x3) o x2 o x3) y (x2 o x1)

o asumimos que en CNF la implicancia viene en el mismo formato de la formula y que CNF solo ocupa, o, y e neg?

Saludos

[juanreutter]

uan formula en CNF son varias clausulas de disjunciones (tipo q v r v not r etc). en dimacs, cada una de esas conjunciones se trata como una formula distinta, en una línea separada: nota que phi AND psi se trata igual que un conjunto {phi,psi} de formulas.

(x1 -> (x2 0 x3) o x2 o x3) y (x2 o x1)

p -> q es not p v q. luego (x1 -> (x2 0 x3) o x2 o x3) y (x2 o x1) es (not x1 o (x2 0 x3) o x2 o x3) y (x2 o x1), que es (not x1 o x2 o x3 o x2 o x3) y (x2 o x1) = (not x1 o x2 o x3) y (x2 o x1). En dimacs usas una linea pa (not x1 o x2 o x3) y otra pa (x2 o x1)

[ljrodriguez1]

Muchas gracias me queda mas claro!

Saludos

[ljrodriguez1]

De esa respuesta puedo asumir que en la representacion en CNF tendra una linea para cada clausula de mi conocimiento negativo? por ejemplo si tengo x1->x2 o x3 x2-> x3 x2 o x3 no x1

entonces mi archivo sera de la forma

not x1 o x2 o x3
not x2 o x3
x2 o x3
not x1

o puede ser que en la transformacion a CNF se limpien proposiciones no necesarias y no se siga exactamente esta transformacion?

Quedo aun con la duda de transformar x1->x2 o x3 a not x1 o x2 o x3 porque aqui x1 podria ser falso y entonces x2 y x3 pueden ser cualquier cosa, cuando en realidad deberia estar obligandolos a ser falso

[ljrodriguez1]

Creo que quiza mi duda viene de que no entiendo bien la implicancia, si tengo

p -> x1 o x2

entonces entiendo que si p es positivo, x1 o x2 debe ser positivo,

Pero si p es negativo entonces obligo a x1 y x2 a ser negativos, o simplemente no se nada de x1 y x2