¿Reducción de tiempo múltiple de ILP a SAT?

14

Entonces, como se sabe, el problema de decisión 0-1 de ILP es NP-completo. Mostrar que está en NP es fácil, y la reducción original fue de SAT; desde entonces, se ha demostrado que muchos otros problemas de NP-Complete tienen formulaciones de ILP (que funcionan como reducciones de esos problemas a ILP), porque ILP es muy útil en general.

Las reducciones de ILP parecen mucho más difíciles de hacer o rastrear.

Por lo tanto, mi pregunta es, ¿alguien sabe una reducción de poli-tiempo de ILP a SAT, es decir, demostrar cómo resolver cualquier problema de decisión de 0-1 ILP usando SAT?

codetaku
fuente

Respuestas:

12

0-1 ILP formulado como:

¿Existe un vector , sujeto a restricciones:x

a11x1+a12x2...+a1nxnb1a21x1+a22x2...+a2nxnb2...am1x1+am2x2...+amnxnbm

Dominio de x: xjxxj{0,1}

Reducción a k-sat:

Primero reduzca al circuito sat:

Comience con la primera fila, cree una variable booleana para representar cada bit en y una variable booleana para x j . Luego haga variable para b 1 . Haz un circuito de suma (elige tu favorito) sumando la fila.a1jxjb1

Luego haga un circuito de comparación, declarando la suma a menos de .b1

Convertir estos dos circuitos a CNF, rellenando los variables, y b 1 , ya que se les da.a1jb1

Repita para todas las filas, pero reutilice las variables entre ellas.xj

El CNF final contendrá todas las restricciones.

Ensalada Realz
fuente
Ah, ya veo ... de alguna manera olvidé la opción de pasar por el circuito satelital ... Muchas gracias por su ayuda.
codetaku
0

Es una especie de respuesta necro a las preguntas ya respondidas y aceptadas, pero quiero señalar que hay una manera realmente más fácil.

Considere que tiene una de las desigualdades como esta:

5x1+2x2+3x36

(1,1,1)(1,1,0)(1,0,1)

(1,1,1)¬(x1x2x3)(¬x1¬x2¬x3)

(¬x1¬x2¬x3)(¬x1¬x2x3) and (¬x1x2¬x3)

Traversing all inequalities and collecting clauses you will get cnf in the end. Often this cnf will be WAY SIMPLER, then one, that results from accepted answer. Cost is harder pre-processing, though.

Konstantin Vladimirov
fuente