Biorąc pod uwagę obwód logiczny na zmiennych (który używa tylko bramek NOT, AND i OR), jaki jest najbardziej skuteczny sposób na wyodrębnienie wzoru logicznego reprezentowanego przez obwód? Czy istnieje algorytm polimeime dla tego problemu?n
10
Odpowiedzi:
Jeśli dobrze rozumiem twoje pytanie, powiedziałbym, że możesz użyć standardowej redukcji z CIRCUIT-SAT do SAT: Reprezentuj każdą bramkę jako nową zmienną, a następnie reprezentuj cały obwód w postaci CNF, przy czym każda klauzula ma postać , gdzie jest nową zmienną, a wzór dla bramki podaje , używając zmiennych dla innych bramek do reprezentowania danych wejściowych. Można tego dokonać przez proste przejście (w czasie liniowym, co jest wyraźnie optymalne).v ϕ( v ↔ ϕ ) v ϕ
Na przykład, jeśli masz trzy wejścia, , i , z bramkami AND łączącymi i a także i oraz bramką OR łączącą ich wyjścia, możesz wprowadzić trzy zmienne reprezentujące bramki - , i - i przepisujemy formułę naZauważ, że zmienna wyjściowa jest dołączona jawnie.x 2 x 3 x 1 x 2 x 2 x 3 v 1 v 2 v 3 ( v 1 ↔ ( x 1 ∧ x 2 ) ) ∧ ( v 2 ↔ ( x 2 ∧ x 3 ) ) ∧ ( v 3 ↔ ( v 1 ∨ v 2 ) ) ∧ v 3x1 x2) x3) x1 x2) x2) x3) v1 v2) v3)
Wprowadzenie do algorytmów Cormena i in. wyjaśnia to szczegółowo w rozdziale o kompletności NP.
źródło