Réduction du poly-temps d'ILP à SAT?

14

Ainsi, comme on le sait, le problème de décision 0-1 d'ILP est NP-complet. Il est facile de montrer qu'il est en NP, et la réduction d'origine provenait de SAT; depuis lors, de nombreux autres problèmes NP-Complete se sont révélés avoir des formulations ILP (qui fonctionnent comme des réductions de ces problèmes en ILP), car ILP est très utile en général.

Les réductions de l' ILP semblent beaucoup plus difficiles à faire moi-même ou à retrouver.

Ainsi, ma question est, est-ce que quelqu'un connaît une réduction du poly-temps de l'ILP à SAT, c'est-à-dire, montrant comment résoudre tout problème de décision ILP 0-1 en utilisant SAT?

codetaku
la source

Réponses:

12

0-1 ILP formulé comme:

Existe-t-il un vecteur , soumis à des contraintes:X

une11X1+une12X2...+une1nXnb1une21X1+une22X2...+une2nXnb2...unem1X1+unem2X2...+unemnXnbm

Domaine de x: XjXXj{0,1}

Réduction en k-sat:

Réduire d'abord en circuit sat:

Commencer avec la première rangée, de créer une variable booléenne pour représenter chaque bit dans et une variable booléenne pour x j . Rendre ensuite variable pour b 1une1jXjb1 . Faites un circuit d'addition (choisissez votre favori) en ajoutant la ligne.

Faites ensuite un circuit de comparaison, déclarant la somme inférieure à b1 .

Convertissez ces deux circuits à CNF, remplissant les des variables et b 1 car ils sont donnés.une1jb1

Répétez l'opération pour toutes les lignes, mais réutilisez les variables entre elles.Xj

Le CNF final contiendra toutes les contraintes.

Realz Slaw
la source
Ah, je vois maintenant ... J'ai en quelque sorte oublié l'option de passer par le circuit assis .... Merci beaucoup pour votre aide.
codetaku
0

C'est une sorte de nécro-réponse à une question déjà répondue et acceptée, mais je tiens à noter qu'il existe un moyen vraiment plus simple.

Considérez que vous avez l'une des inégalités comme celle-ci:

5X1+2X2+3X36

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

(1,1,1)¬(X1X2X3)(¬X1¬X2¬X3) .

(¬X1¬X2¬X3)(¬X1¬X2X3)(¬X1X2¬X3)

Traversant toutes les inégalités et collectant les clauses, vous obtiendrez finalement la cnf. Souvent, ce cnf sera WAY SIMPLER, puis un, qui résulte d'une réponse acceptée. Cependant, le coût est un prétraitement plus difficile.

Konstantin Vladimirov
la source