Problém uspokojivosti obvodu - Circuit satisfiability problem - Wikipedia

Obvod vlevo je uspokojivý, ale obvod vpravo není.

v teoretická informatika, problém uspokojivosti obvodu (také známý jako OKRUH-SAT, CircuitSAT, CSATatd.) je rozhodovací problém rozhodování, zda daný Booleovský obvod má přiřazení svých vstupů, díky nimž je výstup pravdivý.[1] Jinými slovy, ptá se, zda lze důsledně nastavit vstupy do daného booleovského obvodu 1 nebo 0 tak, že obvod vychází 1. V takovém případě se obvod zavolá uspokojivý. Jinak se obvod nazývá neuspokojivý. Na obrázku vpravo lze uspokojit levý obvod nastavením obou vstupů na 1, ale správný okruh je neuspokojivý.

CircuitSAT úzce souvisí s Booleovský problém uspokojivosti (SAT) a také se prokázalo, že je NP-kompletní.[2] Je to prototyp NP-úplného problému; the Cook – Levinova věta se někdy dokazuje na CircuitSAT namísto na SAT a poté se redukuje na další problémy s uspokojivostí, aby se prokázala jejich NP-úplnost.[1][3] Splnitelnost obvodu obsahujícího libovolné binární brány lze rozhodnout včas .[4]

Důkaz NP-úplnosti

Vzhledem k obvodu a uspokojivé sadě vstupů lze vypočítat výstup každé brány v konstantním čase. Proto je výstup obvodu ověřitelný v polynomiálním čase. Circuit SAT tedy patří do třídy složitosti NP. Ukázat NP-tvrdost, je možné postavit a snížení z 3SAT na okruh SAT.

Předpokládejme, že původní vzorec 3SAT obsahuje proměnné , a operátory (AND, OR, NOT) . Navrhněte obvod tak, aby měl vstup odpovídající každé proměnné a bránu odpovídající každému operátorovi. Připojte brány podle vzorce 3SAT. Například pokud je vzorec 3SAT obvod bude mít 3 vstupy, jeden AND, jeden OR a jeden NOT gate. Vstup odpovídající bude před odesláním do brány AND invertováno a výstup brány AND bude odeslán do brány OR pomocí

Všimněte si, že vzorec 3SAT je ekvivalentní obvodu navrženému výše, a proto je jejich výstup stejný pro stejný vstup. Proto má-li vzorec 3SAT uspokojivé přiřazení, bude z příslušného obvodu vycházet 1 a naopak. Jedná se tedy o platnou redukci a Circuit SAT je NP-hard.

Tím je dokončen důkaz, že Circuit SAT je NP-Complete.

Omezené varianty a související problémy

Planární obvod SAT

Předpokládejme, že dostaneme rovinný booleovský obvod (tj. Booleovský obvod, jehož podkladový graf je rovinný ) obsahující pouze NAND brány s přesně dvěma vstupy. Planar Circuit SAT je rozhodovací problém při určování, zda má tento obvod přiřazení svých vstupů, díky nimž je výstup pravdivý. Tento problém je NP-úplný.[5] Ve skutečnosti, pokud se změní omezení tak, aby jakákoli brána v obvodu byla a ANI brána, výsledný problém zůstává NP-úplný.[5]

Okruh UNSAT

Circuit UNSAT je rozhodovací problém při určování, zda daný booleovský obvod vydává false pro všechna možná přiřazení svých vstupů. Toto je doplněk problému Circuit SAT, a proto je Co-NP-kompletní.

Snížení z CircuitSAT

Redukci z CircuitSAT nebo jejích variant lze použít k prokázání NP-tvrdosti určitých problémů a poskytuje nám alternativu k redukci dual-rail a binární logice. Gadgety, které taková redukce potřebuje, jsou:

  • Drátěný gadget. Tento gadget simuluje vodiče v obvodu.
  • Rozdělený gadget. Tento gadget zaručuje, že všechny výstupní vodiče mají stejnou hodnotu jako vstupní vodič.
  • Gadgety simulující brány obvodu.
  • Skutečný terminátor. Tento modul gadget slouží k vynucení výstupu celého obvodu na hodnotu True.
  • Miniaplikace otočení. Tento gadget nám umožňuje podle potřeby přesměrovat vodiče správným směrem.
  • Crossover gadget. Tento gadget nám umožňuje mít dva vodiče křížit se navzájem bez interakce.

Problém odvození hledání min

Tento problém se ptá, zda je možné lokalizovat všechny dané bomby Minolovka prkno. Bylo prokázáno, že je CoNP-Complete prostřednictvím redukce z Circuit UNSAT problému.[6] Gadgety konstruované pro tuto redukci jsou: drátové, dělené, AND a NOT brány a terminátor.[7] Existují tři zásadní pozorování týkající se těchto gadgetů. Nejprve lze dělený gadget použít také jako gadget NOT a gadget turn. Za druhé, postačuje konstrukce gadgetů AND a NOT, protože společně mohou simulovat univerzální bránu NAND. Konečně, protože můžeme simulovat XOR se třemi NANDy, a protože XOR stačí k vytvoření crossoveru, získáme to potřebný crossover gadget.

Tseytinová transformace

Hlavní článek: Transformace tseytinu

The Transformace tseytinu je přímá redukce z Circuit-SAT na SAT. Transformaci lze snadno popsat, pokud je obvod zcela sestaven ze 2 vstupů Brány NAND (A funkčně kompletní sada booleovských operátorů): přiřadit všechny síť v obvodu proměnnou, pak pro každou bránu NAND postavte konjunktivní normální forma doložky (proti1 ∨ proti3) ∧ (proti2 ∨ proti3) ∧ (¬proti1 ∨ ¬proti2 ∨ ¬proti3), kde proti1 a proti2 jsou vstupy do brány NAND a proti3 je výstup. Tyto klauzule zcela popisují vztah mezi třemi proměnnými. Spojení klauzulí ze všech bran s další klauzulí omezující výstupní proměnnou obvodu na true dokončí redukci; přiřazení proměnných splňujících všechna omezení existuje tehdy a jen tehdy, pokud je původní obvod uspokojivý, a jakékoli řešení je řešením původního problému hledání vstupů, které tvoří výstup obvodu 1.[1][8] Konverzace - že SAT je redukovatelná na Circuit-SAT - následuje triviálně přepsáním booleovského vzorce jako obvodu a jeho řešením.

Viz také

Reference

  1. ^ A b C David Mix Barrington a Alexis Maciel (5. července 2000). „Přednáška 7: NP-úplné problémy“ (PDF).
  2. ^ Luca Trevisan (29. listopadu 2001). „Poznámky k přednášce 23: NP-úplnost Circuit-SAT“ (PDF).
  3. ^ Viz také například neformální důkaz uvedený v Scott Aaronson je poznámky z přednášky z jeho kurzu Kvantové výpočty od Demokrita.
  4. ^ Sergey Nurk (1. prosince 2009). „Horní hranice O (2 ^ {0,4058 m}) pro okruh SAT“.
  5. ^ A b „Algorithmic Lower Bounds: Fun with Hardness Proofs at MIT“ (PDF).
  6. ^ Scott, Allan; Stege, Ulrike; van Rooij, Iris (01.12.2011). „Hledání min nemusí být NP úplné, ale přesto je těžké“. Matematický zpravodaj. 33 (4): 5–17. doi:10.1007 / s00283-011-9256-x. ISSN  1866-7414.
  7. ^ Kaye, Richarde. Hledání min je NP-kompletní (PDF).
  8. ^ Marques-Silva, João P. a Luís Guerra e Silva (1999). „Algoritmy pro uspokojivost v kombinačních obvodech založené na zpětném vyhledávání a rekurzivním učení“ (PDF).[trvalý mrtvý odkaz ]