Skrócenie czasu między ILP a SAT?

Tak więc, jak wiadomo, problem decyzyjny ILP 0-1 jest NP-zupełny. Pokazanie tego w NP jest łatwe, a pierwotna redukcja pochodziła z SAT; od tego czasu wykazano, że wiele innych problemów z NP-Complete ma formulacje ILP (które działają jako redukcje tych problemów do ILP), ponieważ ILP jest bardzo przydatna ogólnie.

Redukcje z ILP wydają się znacznie trudniejsze do zrobienia samemu lub wyśledzenia.

Zatem moje pytanie brzmi: czy ktoś zna redukcję czasu wielopunktowego z ILP do SAT, czyli demonstruje, jak rozwiązać problem decyzji 0-1 ILP za pomocą SAT?

0-1 ILP sformułowane jako:

Czy istnieje wektor , z zastrzeżeniem ograniczeń:$\mathbf{x}$

$$\left.\begin{array}{rrrrr|rr} a_{11} x_1 & + &a_{12} x_2 & ... + & a_{1n} x_n\le b_1 \\ a_{21} x_1 & + &a_{22} x_2 & ... + & a_{2n} x_n\le b_2 \\ ...\\ a_{m1} x_1 & + &a_{m2} x_2 & ... + & a_{mn} x_n\le b_m \\ \end{array}\right.$$

$\forall_{x_j \in \mathbf{x}} x_j\in \{0,1\}$

Redukcja do k-sat:

Najpierw zredukuj do obwodu sat:

$a_{1j}$$x_j$$b_1$

$b_1$

$a_{1j}$$b_1$

$x_j$

Ostateczny CNF będzie zawierał wszystkie ograniczenia.

Jest to pewnego rodzaju nekroza odpowiedzi na już udzielone i zaakceptowane pytanie, ale chcę zauważyć, że istnieje naprawdę łatwiejszy sposób.

Rozważ, że masz jedną z takich nierówności:

$5*x_1 + 2*x_2 + 3*x_3 \leq 6$

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

$(1, 1, 1)$$\neg(x_1 \land x_2 \land x_3)$$(\neg x_1 \lor \neg x_2 \lor \neg x_3)$

$(\neg x_1 \lor \neg x_2 \lor \neg x_3)$$(\neg x_1 \lor \neg x_2 \lor x_3)$$(\neg x_1 \lor x_2 \lor \neg x_3)$

Przemierzając wszystkie nierówności i zbierając klauzule, dostaniesz cnf na końcu. Często ten cnf będzie WAY SIMPLER, a następnie taki, który wynika z zaakceptowanej odpowiedzi. Koszt jest jednak trudniejszy w procesie wstępnego przetwarzania.