Uspokojitelnost - Satisfiability

V matematické logice , zahrnující zejména logiku prvního řádu a propoziční počet , jsou uspokojitelnost a platnost elementárními pojmy sémantiky . Formule je splnitelná , jestliže existuje interpretace ( modelu ), který dělá formule pravdivá. Vzorec je platný, pokud všechny interpretace činí vzorec pravdivým. Protiklady těchto pojmů jsou neuspokojitelnost a neplatnost , to znamená, že vzorec je neuspokojitelný, pokud žádná z interpretací nedává vzorec pravdivý, a neplatný, pokud některý takový výklad činí vzorec nepravdivým. Tyto čtyři pojmy jsou vzájemně propojeny takovým způsobem, přesně analogickým Aristotela ‚s náměstím opozice .

Tyto čtyři pojmy lze vztáhnout tak, aby se vztahovaly na celé teorie : teorie je uspokojivá (platná), pokud jeden (všechny) výklady učiní každý z axiomů teorie pravdivým, a teorie je neuspokojivá (neplatná), pokud všechny (jeden) z interpretací činí jeden (y) jeden z axiomů teorie falešný.

Je také možné uvažovat pouze o interpretacích, které činí všechny axiomy druhé teorie pravdivými. Tato generalizace se běžně nazývá teorií modulo uspokojitelnosti .

Otázka, zda je věta v propoziční logice splnitelná, je problémem, který lze rozhodnout ( problém booleovské splnitelnosti ). Obecně nelze rozhodnout, zda je otázka věty logiky prvního řádu splnitelná. V univerzální algebře a rovníkové teorii se k pokusu o uspokojení používají metody přepisování termínů , uzavírání kongruence a unifikace . Zda je určitá teorie rozhodnutelná nebo ne, závisí na tom, zda je teorie bez proměnných nebo za jiných podmínek.

Snížení platnosti na uspokojivost

U klasické logiky s negací je obecně možné znovu vyjádřit otázku platnosti vzorce na takovou, která zahrnuje uspokojitelnost, a to kvůli vztahům mezi pojmy vyjádřenými ve výše uvedeném čtverci opozice. Zejména φ je platné právě tehdy, pokud je ¬φ nevyhovující, což znamená, že je nepravdivé, že ¬φ je splnitelné. Jinak řečeno, φ je splnitelné pouze tehdy, pokud je ¬φ neplatné.

U logiky bez negace, jako je například pozitivní propoziční kalkul , mohou otázky platnosti a uspokojivosti spolu nesouviset. V případě kladného výrokového počtu je problém splnitelnosti triviální, protože každý vzorec je splnitelný, zatímco problém platnosti je co-NP úplný .

Propoziční uspokojivost pro klasickou logiku

V případě klasické výrokové logiky je uspokojivost rozhodovatelná pro výrokové formule. Zejména uspokojivost je NP-úplný problém a je jedním z nejintenzivněji studovaných problémů v teorii výpočetní složitosti .

Uspokojitelnost v logice prvního řádu

U logiky prvního řádu (FOL) je uspokojitelnost nerozhodnutelná . Přesněji řečeno, jedná se o problém doplňující RE-RE, a proto není semidecidable . Tato skutečnost má co do činění s nerozhodnutelností problému platnosti pro FOL. Otázku stavu problému platnosti položil nejprve David Hilbert jako takzvaný Entscheidungsproblem . Univerzální platnost vzorce je polorozhodnutelným problémem Gödelovy věty o úplnosti . Pokud by uspokojitelnost byla také částečně rozhodnutelným problémem, pak by problém existence protimodelů byl také (vzorec má protimodely, pokud je jeho negace uspokojivá). Problém logické platnosti by tedy mohl být rozhodnutelný, což je v rozporu s Církevní -Turingovou větou , což je výsledek uvádějící negativní odpověď na problém Entscheidungsproblem.

Uspokojitelnost v modelové teorii

V modelové teorii je atomový vzorec uspokojivý, pokud existuje sbírka prvků struktury, která činí vzorec pravdivým. Pokud A je struktura, φ je vzorec a a je soubor prvků převzatých ze struktury, které splňují φ, pak se běžně píše, že

A ⊧ φ [a]

Pokud φ nemá žádné volné proměnné, to znamená, že pokud φ je atomová věta a je splněno A , pak se píše

A ⊧ φ

V tomto případě, jeden může také říci, že je modelem pro cp, nebo že φ je pravdivá v A . Pokud T je soubor atomových vět (teorie) splněných A , píše se

A ⊧ T

Konečná spokojenost

Problémem uspokojivosti je problém konečné uspokojivosti , což je otázka určení, zda vzorec připouští konečný model, který ho činí pravdivým. U logiky, která má vlastnost konečného modelu , se problémy splnitelnosti a konečné uspokojivosti shodují, protože vzorec této logiky má model právě tehdy, když má konečný model. Tato otázka je důležitá v matematickém poli teorie konečných modelů .

Konečná uspokojitelnost a uspokojitelnost se nemusí obecně shodovat. Zvažte například logický vzorec prvního řádu získaný jako spojení následujících vět, kde a jsou konstanty : ${\ displaystyle a}$ ${\ displaystyle b}$

${\ displaystyle R (a_ {0}, a_ {0})}$
${\ displaystyle R (a_ {0}, a_ {1})}$
${\ Displaystyle \ forall xy (R (x, y) \ rightarrow \ existuje zR (y, z))}$
${\ Displaystyle \ forall xyz (R (y, x) \ wedge R (z, x) \ rightarrow x = z))}$

Výsledný vzorec má nekonečný model , ale lze ukázat, že nemá žádný konečný model (počínaje skutečností a následováním řetězce atomů, který musí existovat podle třetího axiomu, konečnost modelu by vyžadovala existenci smyčky , což by narušilo čtvrtý axiom, ať už se vrací zpět na nebo na jiný prvek). ${\ Displaystyle R (a_ {0}, a_ {0}), R (a_ {0}, a_ {1}), R (a_ {1}, a_ {2}), \ ldots}$ ${\ displaystyle R (a, b)}$ ${\ displaystyle R}$ ${\ displaystyle a_ {0}}$

Výpočetní složitost rozhodování splnitelnost pro vstupní vzorce v daném logiky se může lišit od toho rozhodování konečných splnitelnost; ve skutečnosti je u některých logik rozhodnutelný pouze jeden z nich .

Pro klasické logiky prvního řádu , konečný satisfiability je rekurzivně spočetný (ve třídě RE ) a undecidable by Trakhtenbrot věty aplikované na negaci vzorce.

Numerická omezení

Numerická omezení se často objevují v oblasti matematické optimalizace , kde člověk obvykle chce maximalizovat (nebo minimalizovat) objektivní funkci podléhající určitým omezením. Ponecháme -li stranou objektivní funkci, základní problém jednoduchého rozhodnutí, zda jsou omezení splnitelná, může být v některých prostředích náročná nebo nerozhodnutelná. Následující tabulka shrnuje hlavní případy.

Omezení	nad realitami	přes celá čísla
Lineární	PTIME (viz lineární programování )	NP-Complete (viz celočíselné programování )
Polynom	rozhodnutelné např. Válcovým algebraickým rozkladem	nerozhodnutelný ( desátý problém Hilberta )

Zdroj tabulky: Bockmayr a Weispfenning .

V případě lineárních vazeb poskytuje následující tabulka úplnější obrázek.

Omezení přes:	racionální	celá čísla	přirozená čísla
Lineární rovnice	PTIME	PTIME	NP-kompletní
Lineární nerovnosti	PTIME	NP-kompletní	NP-kompletní

Zdroj tabulky: Bockmayr a Weispfenning .

Viz také

Poznámky

Reference

Boolos a Jeffrey, 1974. Vypočitatelnost a logika . Cambridge University Press.

Další čtení

Daniel Kroening ; Ofer Strichman (2008). Rozhodovací postupy: Algoritmický úhel pohledu . Springer Science & Business Media. ISBN 978-3-540-74104-6.
A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Příručka uspokojivosti . IOS Press. ISBN 978-1-60750-376-7.

Languages

In other projects