Sağlanabilirlik - Satisfiability

Olarak matematiksel mantık , özellikle, de dahil olmak üzere, birinci derece mantık ve önermeler mantığı , Gerçeklenebilirlik ve geçerlilik elementer kavramlar anlam . Bir formül olan karşılanabilir bir mevcutsa yorumlanması ( Model formülün doğru yapar). Bir formül geçerli tüm yorumların formülün doğru yaparsanız. Bu kavramların karşıtların unsatisfiability ve geçersizlik olduğunu, bir formüldür, edilemezdir yorumların hiçbiri formülün doğru ve yaparsanız geçersiz gibi bazı yorumlama formülü false yaparsa. Bu dört kavram tam olarak benzer bir şekilde birbiriyle ilişkili Aristoteles 'in muhalefet meydanda .

Dört kavram tüm teorilere uygulanmak üzere yükseltilebilir : eğer yorumlardan biri (tümü) teorinin aksiyomlarından her birini doğru yapıyorsa bir teori tatmin edicidir (geçerlidir) ve eğer bir teori, eğer hepsi teorinin aksiyomlarından her birini doğru kılarsa (geçersizdir). (bir) yorum, teorinin aksiyomlarından birini yanlış yapar.

Sadece ikinci bir teorinin tüm aksiyomlarını doğru yapan yorumları düşünmek de mümkündür. Bu genellemeye yaygın olarak tatmin edilebilirlik modulo teorileri denir .

Önerme mantığında bir cümlenin tatmin edilebilir olup olmadığı sorusu karar verilebilir bir problemdir ( boolean tatmin edilebilirlik problemi ). Genel olarak, birinci dereceden bir mantık tümcesinin tatmin edici olup olmadığı sorusu karara bağlanamaz. Gelen evrensel cebir ve equational teorisi , yöntemleri vadeli yeniden yazılması , uyum kapatılması ve birleştirilmesi Gerçeklenebilirlik karar girişimi için kullanılır. Belirli bir teorinin karar verilebilir olup olmadığı, teorinin değişkensiz mi yoksa diğer koşullara mı bağlı olduğuna bağlıdır .

Geçerliliğin tatmin edilebilirliğe indirgenmesi

Olumsuzlamalı klasik mantık için , yukarıdaki karşıtlık karesinde ifade edilen kavramlar arasındaki ilişkilerden dolayı, bir formülün geçerliliği sorununu, tatmin edilebilirliği içeren bir formüle yeniden ifade etmek genellikle mümkündür. Özellikle φ, ancak ve ancak ¬φ tatmin edici değilse geçerlidir, yani ¬φ'nin tatmin edici olduğu yanlıştır. Başka bir deyişle, φ ancak ve ancak ¬φ geçersizse tatmin edicidir.

Olumlu önermeler hesabı gibi olumsuzlama içermeyen mantıklar için geçerlilik ve tatmin edilebilirlik soruları ilgisiz olabilir. Olumlu önermeler hesabı durumunda , geçerlilik sorunu eş-NP tamamlanırken her formül karşılanabilir olduğundan, karşılanabilirlik sorunu önemsizdir .

Klasik mantık için önermesel tatmin edilebilirlik

Klasik önerme mantığı durumunda, önerme formülleri için tatmin edilebilirlik kararlaştırılabilir. Özellikle, tatmin edilebilirlik NP-tam bir problemdir ve hesaplama karmaşıklığı teorisinde en yoğun çalışılan problemlerden biridir .

Birinci dereceden mantıkta tatmin edilebilirlik

İçin birinci derece mantık (FOL), Satisfiability olan undecidable . Daha spesifik olarak, birlikte-RE-tamamlanmış bir problemdir ve bu nedenle yarı karar verilemez . Bu gerçek, FOL için geçerlilik sorununun karar verilemezliği ile ilgilidir. Geçerlilik sorununun statüsü sorunu ilk olarak David Hilbert tarafından sözde Entscheidungsproblem olarak ortaya atılmıştır . Bir formülün evrensel geçerliliği, Gödel'in tamlık teoremi tarafından yarı karar verilebilir bir problemdir . Eğer tatmin edilebilirlik aynı zamanda yarı-karar verilebilir bir problem olsaydı, o zaman karşı-modellerin mevcudiyeti problemi de olurdu (bir formülün, eğer olumsuzlaması tatmin edici ise, karşı-modelleri vardır). Dolayısıyla, Entscheidungsproblem için olumsuz cevabı belirten bir sonuç olan Church-Turing teoremi ile çelişen mantıksal geçerlilik sorunu karar verilebilir olacaktır .

Model teorisinde tatmin edicilik

Gelen modeli teorisi , bir atom formülü bir elemanlarının bir koleksiyon varsa karşılanabilir olduğunu yapısına formülün doğru hale. Eğer bir bir yapı olup, φ bir formüldür ve bir yapıdan alınan elemanlarının bir koleksiyonudur, tatmin cp ki, o zaman bu genellikle yazılıdır

Bir ⊧ φ [a]

φ'nin serbest değişkeni yoksa, yani φ atomik bir cümleyse ve A ile karşılanıyorsa , o zaman yazar

bir ⊧ φ

Bu durumda, bir de söyleyebiliriz Bir cp için bir model olduğu veya bu φ olduğu doğrudur içinde A . Eğer T memnun atomik cümle (bir teori) topluluğudur A , bir yazma

bir ⊧ T

sonlu tatmin edilebilirlik

Tatmin edilebilirlikle ilgili bir problem , bir formülün onu doğru yapan sonlu bir modeli kabul edip etmediğini belirleme sorusu olan sonlu tatmin edilebilirlik problemidir . Sonlu model özelliğine sahip bir mantık için, tatmin edilebilirlik ve sonlu tatmin edilebilirlik sorunları çakışır, çünkü bu mantığın formülünün bir modeli varsa ve ancak sonlu bir modeli varsa. Bu soru, sonlu model teorisinin matematiksel alanında önemlidir .

Sonlu tatmin edilebilirlik ve tatmin edilebilirliğin genel olarak çakışması gerekmez. Örneğin, dikkate birinci dereceden mantığı olarak elde formüle birlikte aşağıdaki cümle arasında ve vardır sabitleri : ${\görüntüleme stili bir}$${\görüntüleme stili b}$

• ${\displaystyle R(a_{0},a_{0})}$
• ${\displaystyle R(a_{0},a_{1})}$
• ${\görüntüleme stili \için tüm xy(R(x,y)\sağ ok \zR(y,z))}$
• ${\displaystyle \forall xyz(R(y,x)\kama R(z,x)\sağ ok x=z))}$

Ortaya çıkan formül sonsuz modele sahiptir , ancak sonlu bir modeli olmadığı gösterilebilir (olgudan başlayarak ve üçüncü aksiyom tarafından var olması gereken atom zincirini takip ederek , bir modelin sonluluğu bir döngünün varlığını gerektirir. , bu, dördüncü aksiyomu ihlal eder, ister geri dönsün, ister farklı bir eleman üzerinde olsun). ${\displaystyle R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots }$${\görüntüleme stili R(a,b)}$${\görüntüleme stili R}$ ${\ Displaystyle a_{0}}$

Hesaplama karmaşıklığı , belirli bir mantık, giriş formül Gerçeklenebilirlik karar verme sonlu Gerçeklenebilirlik karar verme farklı olabilir; aslında, bazı mantıklar için bunlardan sadece biri kararlaştırılabilir .

Klasik birinci dereceden mantık için , sonlu tatmin edilebilirlik özyinelemeli olarak sayılabilir ( RE sınıfında ) ve formülün olumsuzlamasına uygulanan Trakhtenbrot teoremi tarafından karar verilemez .

Sayısal kısıtlamalar

Sayısal kısıtlamalar genellikle , bazı kısıtlamalara tabi olan bir amaç fonksiyonunu maksimize etmek (veya minimize etmek) isteyen matematiksel optimizasyon alanında ortaya çıkar . Bununla birlikte, amaç fonksiyonunu bir kenara bırakırsak, temel mesele kısıtlamaların tatmin edilebilir olup olmadığına karar vermek bazı durumlarda zorlayıcı veya karar verilemez olabilir. Aşağıdaki tablo ana durumları özetlemektedir.

kısıtlamalar	gerçeklerin üzerinde	tamsayılar üzerinde
Doğrusal	PTIME ( doğrusal programlamaya bakın )	NP-tamamlandı (bkz. tamsayı programlama )
Polinom	örneğin Silindirik cebirsel ayrıştırma yoluyla karar verilebilir	karar verilemez ( Hilbert'in onuncu problemi )

Tablo kaynağı: Bockmayr ve Weispfenning .

Doğrusal kısıtlamalar için, aşağıdaki tabloda daha eksiksiz bir resim sunulmaktadır.

Üzerinde kısıtlamalar:	rasyoneller	tam sayılar	doğal sayılar
Doğrusal denklemler	PTIME	PTIME	NP-tamamlandı
Doğrusal eşitsizlikler	PTIME	NP-tamamlandı	NP-tamamlandı

Tablo kaynağı: Bockmayr ve Weispfenning .

Ayrıca bakınız

• 2-tatmin edilebilirlik
• Boolean tatmin edilebilirlik sorunu
• Devre tatmini
• Karp'ın 21 NP-tam sorunları
• Geçerlilik
• Kısıtlama memnuniyeti
• tatmin edici

Notlar

Referanslar

• Boolos ve Jeffrey, 1974. Hesaplanabilirlik ve Mantık . Cambridge Üniversitesi Yayınları.

daha fazla okuma

• Daniel Kroning ; Ofer Strichman (2008). Karar Prosedürleri: Algoritmik Bir Bakış Açısı . Springer Bilim ve İş Medyası. ISBN'si 978-3-540-74104-6.
• A. Biere; M. Heule; H.van Maaren; T. Walsh, ed. (2009). Memnuniyet El Kitabı . IOS Basın. ISBN'si 978-1-60750-376-7.