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?
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:
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.
fuente