واگشایی (Resolution) و برهان مکانیکی قضیه
منطق و فرامنطق
درآمد به منطق
«بهنظر میرسد اشیای ریاضی، نابسته به تعاریف و ساختههای ذهنی ما، بهعنوان اشیایی واقعی وجود دارند.»
نزدیک به مضمون از کورت گودل — «مسئله پیوستار کانتور چیست؟ — ۱۹۴۷. [پیوستار کانتور]
این نگاه افلاطونی در قالب «جهان فون نویمان» صورتبندی شده است. جایی که همه مجموعهها در یک کل ایستا و بیزمان گرد میآیند. قواعد منطقی واگشایی (Resolution) و جدایش (Separation) را میتوان پلی میان این جهان ریاضی بیزمان و اجرای مکانیکی آن در زمان دانست. تنها هنگامی که روی سیلیکون اجرا میشود، به پناهندگی در زمان و مکان* تن میدهد.
[* عبارت «پناهندگی در زمان و مکان» تولید شده توسط هوش مصنوعی است.]
«هر چه نظریه علمیتر، از ریسک ابطالپذیری برخوردارتر. هر چه ابطالپذیرتر، جرئت علمی بیشتر.»
نزدیک به مضمون از کارل پوپر (در «منطق اکتشاف علمی» - ۱۹۳۴)
Popper, Karl. 2002. The Logic of Scientific Discovery. London: Routledge, pp 102-103.
واگشایی (Resolution) و برهان مکانیکی قضیه
• مقدمه | • روش واگشایی و اثبات مکانیکی قضیه |
• صورت نرمال (Normal form) | • قاعده واگشایی (Resolution rule) |
• چند تعریف: لیترال، بندواره | • ناسازگی دو بندواره در چند لیترال |
• صورت نرمال نقضی (Negation Normal Form) | • قضیه پایستاری صدق پذیری واگشایی (Satisfiability Preservation Theorem for Resolution) |
• الگوریتم غیربازگشتی (چرخه کراندار) برگردان فرمول به NNF | • افراز مجموعه متناهی بندوارهها (قاعده جدایش `p` / `p`-Separation) |
• الگوریتم بازگشتی (Recursive) برگردان فرمول به NNF | • فراروند واگشایی (Resolution procedure) |
• آزمایشگاه منطق: برگردان فرمول به NNF | • الگوریتم واگشایی (Resolution algorithm) |
• اصل همزادی (Duality) | • مثال برای فراروند واگشایی |
• صورت نرمال عطفی (Conjunctive Normal Form) | • آزمایشگاه منطق: الگوریتم واگشایی (Resolution Algorithm) |
• صورت نرمال فصلی (Disjunctive Normal Form) | • استواری روش واگشایی (The soundness of resolution method) |
• الگوریتم برگردان فرمول به DNF / CNF | • تمامیت وازنشی واگشایی در منطق گزارهای (Resolution Refutation Completeness) |
• آزمایشگاه منطق: برگردان فرمول به صورتهای نرمال | • کارآمدی الگوریتم واگشایی (Resolution algorithm efficiency) |
■ مقدمه
در این قسمت با مفاهیم صورتهای نرمال (Normal Forms) در منطق گزارهها آشنا میشویم. صورتهای نرمال را میتوان بهمنزله «ساختارهای صوری استاندارد» برای گزارههای منطقی در نظر گرفت که آنها را برای تحلیل صوری، مقایسه و پردازش ماشینی مناسبتر و یکنواتر میسازند. تمرکز ما بهطور خاص بر سه صورت مهم است: نرمال نقضی (Negation Normal Form – NNF)، نرمال عطفی (Conjunctive Normal Form – CNF) و نرمال فصلی (Disjunctive Normal Form – DNF).
در ادامه، ابتدا یک الگوریتم برای برگردان (بازنویسی) هر فرمول خوش-ساخت به NNF ارائه میکنیم و گامبهگام نشان میدهیم که این برگردان چگونه انجام میشود و چرا ساختار منطقی فرمول را حفظ میکند. سپس بر پایه همین پنداشت، یک الگوریتم رایج و پرکاربرد برای برگردان فرمولها به CNF معرفی میکنیم. الگوریتمی که نقش محوری در ارائه فرمولها بعنوان ورودی به فراروند واگشایی (Resolution procedure)، که در ادامه خواهیم دید، دارد. برای تمرین و فهم عمیقتر این برگردانها، دو آزمایشگاه عملی نیز در نظر گرفته شده است تا بتوان برگردان فرمولهای مختلف به NNF و CNF را بهصورت تعاملی تجربه کرد.
پس از آن، به مفهوم همزادی (دوگانگی - Duality) میپردازیم. مفهومی که یک تقارن ژرف میان رابطهای منطقی عطفی و فصلی را آشکار میکند و توضیح میدهد که چگونه میتوان بسیاری از نتایج را در دو «نسخه همزاد» آنها صورتبندی کرد. این دیدگاهِ همزاد، درک ما از ساختار منطق گزارهها و رفتار صورتهای نرمال را غنیتر میسازد.
در پایان، قاعده واگشایی (Resolution rule) و فراروند واگشایی (Resolution procedure) را معرفی خواهیم کرد. قاعده واگشایی یک قاعده استنتاج واحد، ساده و در عین حال بسیار توانمند است که وقتی بر فرمولهای بازنویسیشده در قالب CNF اعمال میشود، هستهٔ اصلی برهان مکانیکی قضایا در منطق گزارهها را شکل میدهد. بدین ترتیب، خواهیم دید که چگونه برگردانهای ساختاری صوری میتوانند بهگونه الگوریتمی پیادهسازی شوند و توسط کامپیوترها برای اثبات مکانیکی اعتبار استدلالها به کار روند.
■ صورت نرمال (Normal form)
در منطق، وقتی در مورد «صورت نرمال» صحبت میکنیم، منظورما یک روش استاندارد یا پذیرفته برای نگارش فرمولها است به قسمی که:
- ۱- همه آنها از یک نظم نحوی خاص پیروی کنند.
- ۲- فرمولهای منطقی همارز مختلف را میتوان به این شکل یکنواخت بازنویسی کرد.
بنابراین صورت نرمال یک فرمول خوش-ساخت عبارت است از یک بازنمایی سیستماتیک و از نظر نحوی محدود آن از فرمول، بدون تغییر معنی آن فرمول (یعنی یک همارزی منطقی). این امر استدلال، اثبات و نوشتن الگوریتمها را بسیار آسانتر میکند. ما در ادامه سه صورت نرمال (نقضی، عطفی و فصلی) را معرفی و روش برگردان فرمول را به هر یک از این سه صورت نشان میدهیم.
■ چند تعریف: لیترال، بندواره
■ لیترال (Literal)
به یک اتم نیز نقیض آن یک لیترال میگوییم. برای نمونه `p, ~p, q` و مانند آنها لیترال هستند.
■ بندواره (Clause)
یک بندواره (Clause) یک ترکیب فصلی متناهی (که میتواند خالی هم باشد) از لیترالها است. برای نمونه:
`p`
`~p`
`(p vv ~p vv q)`
`(p vv r vv ~q)`
و مانند آنها بندواره هستند.
یک بندواره را به صورت مجموعهای از لیترالها نمایش میدهند. برای مثال، بندوارههای بالا را میتوان به شکل زیر نوشت.
`{p}=p`
`{~p}=~p`
`{p, ~p, q}= p vv ~p vv q`
`{p, r, ~q}=p vv r vv ~q`
توجه: در این بخش (برهان مکانیکی)، نقیض `q`، یعنی `~q`، «لیترال متمم» نامیده و با `bar q` نشان داده میدهیم. دراین صورت نماد (`vv`) در بندواره حذف میشود. بنابراین میتوانیم بنویسیم:
`{p}=p`
`{~p}=~p=barp`
`{p, ~p, q}= p vv ~p vv q=pbar p q`
`{p, r, ~q}=p vv r vv ~q=pr barq`
■ بندواره یکانی (Unit Clause)
بندواره یکانی بندوارهای است که دقیقاً یک لیترال داشته باشد.
■ بندواه تهی (Empty Clause)
یک بندواره تهی یک مجموعه لیترال تهی است. بندواره تهی را معمولاً با `color(red)(_|_)` یا یک مجموعه تهی {} (نیز گاهی با `square`) نشان میدهند.
بندواره تهی، `_|_`، صدق پذیر نیست. زیرا:
یک بندواره صدق پذیر است اگر تحت تعبیری حداقل یک لیترال در آن درست باشد. فرض کنید `cc"I"` یک تعبیر دلخواه باشد. از آنجایی در `_|_` لیترالی نیست، پس هیچ لیترالی از بندواره تحت `cc"I"` درست نیست و چون `cc"I"` یک تعبیر دلخواه است، پس `_|_` صدقپذیر نیست.
■ بندواره بدیهی (Trivial Clause)
تعریف: یک بندواره بدیهی (trivial) است اگر شامل یک جفت لیترال متناقض باشد.
از آنجایی که یک بندواره بدیهی توتولوژی است `(p ∨ ~p ≡ true)`، میتوان آن را از مجموعهای از بندواره بدون تغییر مقدار ارزش فرمول حذف کرد. بنابراین اگر `S` مجموعهای از بندواره باشد و `C ∈ S` یک بندواره بدیهی باشد، آنگاه `S −{C}` منطقاً همارز `S` است. بنابراین یک فرمول در قالب بندواره را میتوان با حذف بندوارههای بدیهی (trivial) ساده کرد.
■ صورت بندوارهای (Clausal form)
به ترکیب عطفی بندوارهها یک صورت بندوارهای میگوییم. برای نمونه:
(I): `(p vv ~p vv q) ^^ (p vv r vv ~q)`
یا بگونه کوتاهتر:
(II): `p bar p q ^^pr bar q`
و مانند آنها صورت بندوارهای هستند.
یک صورت بندوارهای را به صورت مجموعهای از بندوارهها نیز مینویسند که در آن جداکننده `'^^'` حذف و جداکننده معمول عناصر مجموعه جای آن مینشیند. برای مثال، صورت بندوارهای بالا (I و II) را میتوان به شکل زیر نوشت.
(III): `{p barp q, p r barq}`
اگر `l` یک لیترال باشد، `l^c` متمم آن است و در این صورت: اگر `l = p` ، آنگاه `l^c = bar p` و اگر `l = bar p` ، آنگاه `l^c = p`.
■ صورت نرمال نقضی (Negation Normal Form)
صورت نرمال نقضی (NNF) را بگونه استقرایی به شیوه زیر تعریف میکنیم:
- هر لیترال در صورت NNF است،
- `top` و `bot` در صورت NNF هستند،
- اگر فرمولهای `α` و `β` در صورت NNF باشند آنگاه
- `α ^^ β` در صورت NNF هستند،
- `α vv β` در صورت NNF هستند،
- یک فرمول در صورت NNF است اگر و تنها اگر بتوان نشان داد بر مبنای قواعد ۱ تا ۳ به دست آمده است.
به عبارت دیگر: یک فرمول خوش-ساخت در صورت نرمال نقضی (NNF) است اگر و تنها اگر فاقد رابطهای شرطی و دو شرطی `(supset, equiv)` باشد و تمام رابطهای نقیض در فرمول فقط بر اتمها کار زده شده باشند.
برای مثال `(~p∨q)∧r` و `p∧(~q∨(s∧~t))` در صورت NNF هستند. ولی فرمولهای `~(p∨q)` و `p → q` در صورت NNF نیستند.
در ادامه این قسمت، نشان میدهیم که صورتهای نرمال نقضی (NNF) به عنوان پایهای ضروری برای تبدیل یک فرمول به دو قالب خاص عمل میکند: صورتهای نرمال عطفی و فصلی.
پیش از برگردان فرمولی به هر یک از این دو صورت، ابتدا باید به NNF برگردان شود. همچنین بررسی خواهیم کرد که چگونه این صورتها زیربنای روند اثبات مکانیکی هستند و نقش مهمی در اعتبار سنجی صوری قضیه ایفا میکنند.
■ الگوریتم غیربازگشتی (چرخه کراندار) برگردان فرمول به NNF
- حذف رابطها دو شرطی ('`equiv`') و شرطی ('`sup`') با کارزدن همارزیهای مادی و استلزام مادی:
- رویدادهای `(p sup q)` را با `(~p vv q)` جایگزین کنید.
- رویدادهای `(p equiv q)` را به `((p sup q) ^^ (q sup p))` برگردانید، سپس این عطفی را با `((~p ∨ q) ∧ (~q ∨ p))` جایگزین کنید،
- پیش راندن رویدادهای رابط '~' در فرمول به بلافاصله قبل از اتمها با کارزدن چرخهای نقض دوگانه و قضایای دمورگان:
- به طور چرخهای، قواعد زیر را برای پیشراندن همه رابطهای نقیض (~) به سمت داخل بکار ببرید:
- نقض دوگانه: `~(~p)` با `p` جایگزین کنید،
- قوانین دمورگان:
- `~(p ^^ q)` با `~p vv ~q` جایگزین کنید،
- `~(p vv q)` با `~p ^^ ~q` جایگزین کنید،
- مراحل ۱ و ۲ را تکرار کنید تا فرمول فقط شامل عملگرهای `~`، `^^` و `vv` باشد، نیز همه رابطها قبل از اتمها ظاهر شوند.
■ الگوریتم بازگشتی (Recursive) برگردان فرمول به NNF
تابع To_NNF(Formul) به صورت بازگشتی Formul (فرمول خوش-ساخت) منطق گزارهای را به صورت نرمال نقضی (NNF) برگردان میکند.
- حالت مبنایی: اگر `φ` یک لیترال است، `φ` هم اکنون یک NNF است، بنابراین خود `φ` بعنوان خروجی برگردانده شود.
- حالتهای بازگشتی:
- اگر `φ` به شمای `(β sup γ)` است:
- بطور بازگشتی فرمول To_NNF`(~β vv γ)` فرخوانی شود.
- اگر `φ` به شمای `(β ≡ γ)` است:
- بطور بازگشتی فرمول To_NNF`((~β vv γ) ^^ (~γ vv β))` فرخوانی شود.
- اگر `φ` به شمای `~(β ^^ γ)` است:
- بطور بازگشتی فرمول To_NNF`(~β vv ~γ) ` فراخوانی شود.
- اگر `φ` به شمای `~(β vv γ)` است:
- بطور بازگشتی فرمول To_NNF`(~β ^^ ~γ) ` فراخوانی شود.
- اگر `φ` به شمای `~(~β)` است:
- بطور بازگشتی فرمول To_NNF`(β) ` فراخوانی شود.
- اگر `φ` به شمای `(β ^^ γ)` است:
- فرمولهای To_NNF`(β) ` و To_NNF`(γ) ` بطور بازگشتی فراخوانی شوند.
- To_NNF`(β) ^^ `To_NNF`(β)` به عنوان نتیجه برگردانده شود.
- اگر `φ` به شمای `(β vv γ)` است:
- فرمولهای To_NNF`(β) ` و To_NNF`(γ) ` بطور بازگشتی فراخوانی شوند.
- To_NNF`(β) vv `To_NNF`(β)` به عنوان نتیجه برگردانده شوند.
■ آزمایشگاه منطق: برگردان فرمول به NNF
آزمایشگاه
برگردان فرمول به صورت نرمال نقضی
Negation Normal Form
برای ورود به آزمایشگاه الگوریتم برگردان فرمول به NNF روی دکمه
کلیک کنید.
■ اصل همزادی (Duality)
قضیه همزادی:
فرض کنید `β` یک صورت گزارهای باشد که فقط رابطهای `~`، `^^` و `vv` در آن بکار برده شده باشند. نیز فرض کنید `β'` با جایگزینی هر مورد `^^` با `vv` و هر مورد `vv` با `^^` در `β` بدست آمده باشد.
در این صورت:
آ- `β` یک توتولوژی است اگر و تنها اگر `~β′` یک توتولوژی باشد.
ب- اگر `β sup gammaس` یک توتولوژی باشد، آنگاه `gamma′ sup β′` نیز چنین است، و اگر `β equiv gamma` یک توتولوژی باشد، آنگاه`β' equiv gamma'` نیز چنین است. (در اینجا فرض شده که `gamma` فقط شامل رابطهای `~`، `^^` و `vv` است.) ⤓
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p 16.
اثبات برهانی را میتوانید در
Colin Howson. Logic with trees. An introduction to symbolic logic. 6th, ed, Routledge. 2005. p 44.
ببینید.
اثبات:
آ-
اگر `β` یک توتولوژی باشد، نتیجه جایگزینی همه حروف گزارهای با نقیض آنها، یک توتولوژی است. اکنون با کارزدن همارزیهای منطقی زیر:
`~(cc"B" vv cc"C") ≡^T (~cc"B") ^^ (~cc"C")`
`~(cc"B" ^^ cc"C") overset(T)≡ (~cc"B") vv (~cc"C")`
همه رابطهای نقیض را به سمت بیرون حرکت دهیم. نتیجه توتولوژی `~β′` خواهد بود.
ب-
برعکس، اگر `~β′` یک توتولوژی باشد. `gamma` را به صورت `~β′` بگیرید. اکنون طبق بند یکم `~gamma` یک توتولوژی است. اما `~gamma` همان `~ ~β` است.
■ نتیجه: اصل همزادی
اگر `β` فرمولی باشد که فقط در آن رابطهای `~`، `^^` و `vv` بکار رفته باشند و `β^**` با جابجایی `^^` و `vv` و تبدیل هر حرف گزارهای به نقیض آن از `β` بهدست آید، `β^**` منطقاً همارز `~β` است.
اثبات: نتیجه مستقیم قضیه همزادی.
مثال:
۱- `(p ^^ q)^** = (~p vv ~q)` و داریم `~(p ^^ q)^**` `≡^T` `(p ^^ q)`
۲- `((p vv ~q) ^^ (q ∨ p)) ≡^T ~((~p ^^ q) vv (~q ^^ ~p))`
■ صورت نرمال عطفی (Conjunctive Normal Form)
صورت نرمال عطفی (CNF) را بگونه بازگشتی به شیوه زیر تعریف میکنیم:
- هر بندواره یک CNF است،
- اگر فرمولهای `α` و `β` هر یک CNF باشند آنگاه `α ^^ β` یک CNF است.
- یک فرمول یک CNF است اگر و تنها اگر بتوان نشان داد بر مبنای قواعد ۱ و ۲ به دست آمده است.
به عبارت دیگر:
به فرمولی با صورت `C_۱ ^^ C_۲ ^^ ...^^ C_m` که در آن هر `C_i` یک بندواره (Clause - ترکیب فصلی لیترالها) باشد یک صورت نرمال عطفی میگوییم (m عدد طبیعی بزرگتر از صفر).
مثال:
(p ∨ ~q) `^^` (q ∨ p) `^^` (~q ∨ ~s ∨ q)
در این مثال m = ۳ است و بندوارهها عبارتند از هستند:
`C_۱: (p vv ~q), C_۲: (q vv p), C_۳: (~q vv ~s vv q)`.
`{pbarq, qp, barqbarsq}`
■ صورت نرمال فصلی (Disjunctive Normal Form)
به فرمولی با صورت
A۱∨A۲∨ . . . ∨Am
که در آن هر Ai یک صورت عطفی لیترالها است یک صورت نرمال فصلی (DNF) میگوییم. (m؛ عدد طبیعی بزرگتر از صفر).
برای مثال صورت:
`(p ^^ ~q) vv (q ^^ p) vv (~q ^^ ~s)`
یک صورت نرمال فصلی است که در آن
`A_۱ :` `(p ^^ ~q)`, `A_۱ :` `(q ^^ p)`, `A_۱ :` `(~q ^^ ~s)`
صورتهای عطفی لیترالها هستند.
■ الگوریتم برگردان فرمول به DNF / CNF
هر فرمول خوش-ساخت گزارهای قابل برگردان به صورتهای نرمال عطفی و فصلی است. روند زیر با کارآمدی برگردان به DNF/CNF نجام میدهد:
فرض کنید `φ` یک فرمول خوش-ساخت گزارهای باشد.
- `φ` را به NNF برگردان کنید.
- صورت نرمال را با کارزدن چرخهای همارزیهای پخش پذیری و انجمنی بر روی نتیجه گام ۱ به دست آورید.
مثال:
▢
≡
≡
≡
≡
`(p vv ~q) ⊃ r`
`~(p vv ~q) ∨ r`
`(~p ^^ ~(~q)) ∨ r`
`(~p ^^ q) vv r`
`(p ∨ ~q) vv ~r`
مثال:
▢
≡
≡
≡
≡
≡
≡
≡
≡
≡
`(p ^^ (q ⊃ r) ⊃ s)`
`(p ^^ (~q vv s)) ⊃ s`
`~(p ^^ (~q vv s)) vv s`
`(~p vv ~(~ q vv r )) vv s`
`(~p vv ( q ^^ ~r)) vv s`
`((~p vv q) ^^ (~p vv ~r)) vv s`
`s vv ((~p vv q) ^^ (~p vv ~r))`
`(s vv (~p vv q) ^^ (s vv (~p vv ~r))`
`(s vv ~p vv q) ^^ (s vv ~p vv ~r)`
`(~s ^^ p ^^ ~q) vv (~s ^^ p ^^ r)`
■ آزمایشگاه منطق: برگردان فرمول به صورتهای نرمال
آزمایشگاه
برگردان فرمول به صورتهای نرمال
Converting formulas to normal forms
برای ورود به آزمایشگاه الگوریتم برگردان فرمول به CNF روی دکمه
کلیک کنید.
■ روش واگشایی و اثبات مکانیکی قضیه
تاکنون برای اثبات اعتبار یا بیاعتباری یک استدلال تابع-ارزش روشهای جدول ارزش، جدول ارزش کوتاهتر، برهان صوری اعتبار و روش درخت معنا را مشاهده کردهایم. این قسمت «روش واگشایی منطقی / Resolution method» (نیز نامیده به «روش تفکیک» یا «روش رزولوشن») را به عنوان سنگ بنای برهان خودکار قضیه معرفی میکند. روش واگشایی توسط جان آلن رابینسون در سال ۱۹۶۵ معرفی شد. این روش یک چارچوب الگوریتمی برای تعیین سیستماتیک صدق پذیری یا صدق ناپذیری را فراهم میکند. [مراد از یک چارچوب الگوریتمی یک طرح یا الگوی ساختاریافته و قابل استفاده مجدد است که به جای یک الگوریتم خاص و انعطافناپذیر، یک رویکرد کلی برای حل دستهای از مسائل ارائه میدهد. این چارچوب به عنوان یک ساختار انتزاعی منطقی اجزای کلیدی و تعاملات آنها را تعریف میکند و به گسترندگان (Developers) امکان میدهد تا آن را برای موارد استفاده خاص تطبیق یا گسترش دهند. و این در حالی است که صحت برهان و کارآمدی پابرجا میماند].
■ تمامیت وازنشی (Refutation-Completeness)
روش واگشایی دارای تمامیت وازنشی است، یعنی اگر فرمولی صدق پذیر نباشد آنگاه واگشایی به تناقض منجر میشود. توجه داریم که روش واگشایی تصمیمپذیر است. به عبارت بهتر:
یک دستگاه برهانی (مانند یک نظریه برهان) دارای تمامیت وازنشی است که بتواند از هر مجموعهای از مقدمات که صدق پذیر نیست، یک ناسازگی (وازنش) استخراج کند (یعنی اگر مقدمات ناسازگار باشند، سیستم این موضوع را با استخراج تناقضی مانند `color(red)(bot)` تشخیص دهد).
روش واگشایی در بنیاد یک فراروند (Procedure) برهانی (↝) و بنیادین و کارساز در جستجو برای یافتن برهان نحوی قضیه در منطق کلاسیک (دو ارزشی) است. این روش به عنوان پایه بسیاری از تکنیکهای برهان، به ویژه در اثبات قضیه مبتنی بر وازنش منطقی (Refutation)، عمل میکند. در واقع، برهان از روش وازنش جستجوی برهان را به جستجوی تناقض برمیگرداند. برهان غیرمستقیم اعتبار که آن را با تفصیل در قسمت ۱۱ فصل ۱۰ کتابدرآمد به منطق دیدیم، نیز روش درخت معنایی هر دو از تکنیکهای وازنشی هستند.
■ قاعده واگشایی (Resolution rule)
شمای قاعده واگشایی از قرار زیر است:
`p vv q` `not q vv r`
R1: —————————————
`p vv r`
شِمای بالا را میتوان به صورت زیر نوشت (استلزام مادی) تا برای خواندن صورت آشکارتر داشته باشد:
`not p => q` `q => r`
R2: —————————————
`not p => r`
■ واگشایی (Resolution) و واگشا (Resolvent)
فرض کنید `C_۱` و `C_۲` بندوارههایی باشند بقسمی که داشته باشیم: `l ∈ C_۱` و `l^c ∈ C_۲`. آنگاه به بندوارههای `C_۱` و `C_۲`، که در جفت لیترالهای `l` و `l^c` ناسازند، بندوارههای ناسازه (Opposing clauses) میگوییم. در این صورت به `C` از قرار:
`C = (C_۱ − {l}) ∪ (C_۲ − {l^c})`
واگشای `C_۱` و `C_۲` گفته میشود و مینویسیم:
`Res (C_۱, C_۲)= (C_۱ − {l}) ∪ (C_۲ − {l^c})`.↧
Mordechai Ben-Ari. Mathematical Logic for Computer Science. 3th, ed, Springer, .2012. 4.24. p 80.
به عبارت آشناتر:
اگر
`C_۱=(A_1∨⋯∨L∨⋯∨A_m)`
و
`C_۲=(B_۱∨⋯∨~L∨⋯∨B_n)`
آنگاه
`Res(C_۱, C_۲)=``(A_۲∨⋯∨A_m∨B۱∨⋯∨B_n)`.
مثال: جفت بندوارههای `C_1 = ab barc` و `C_2 = bc bare` در لیترالهای `c` و `bar c` ناسازه هستند و واگشای (Resolvent) آنها، `C`، از قرار زیر است.
(I). `C = (ab bar color(red)(c) − {barc}) ∪ (bcolor(red)(c) bare − {c})` = `ab ∪ b bare = ab bare`.
عبارت (I) در بالا را میتوان به شیوه زیر کوتاهتر نوشت:
`Res^c(ab bar c, bc bar e)=ab bar e`.
بالا-نویس `c` در `Res^c` نشاندهنده نقش واگشایی `c` است.
در ادامه نشان میدهیم در منطق گزارهای کلاسیک جدید، قاعده واگشایی به تنهایی برای اثبات صدق ناپذیری مجموعهای از فرمولها کافی است اگر و تنها اگر فرمولها به صورت CNF نوشته شده باشند.
■ ناسازگی دو بندواره در چند لیترال
لم:
اگر دو بندواره در بیش از یک لیترال ناساز باشند، واگشای آنها یک بندواره بدیهی است.
اثبات:
فرض کنید `C_1` و `C_2` بندوارههایی باشند که روی متغیرهای `v` و `w` با هم ناسازند. بنابراین، `C_1` دارای لیترالهایی است که در آنها `v` و `w` هستند. نیز، `C_2` دارای لیترالهای `bar v` و `barw` (متمم `v` و `w`) هستند. پس، واگشایی روی `v`، لیترالهای `v` و `bar w` را باقی میگذارد. یعنی، حاصل شامل `(w ∨ ~w)` خواهد بود. اما، `(w ∨ ~w)` یک توتولوژی است. پس، حاصل واگشایی یک بندواره بدیهی است.
مثال ۱:
`C_1: (AB)`
`C_2: (barA barB)`
ناسازی روی متغیرهای `A` و `B`.
`Res^A(C_1, C_2) = (B ∨ ~B) →` توتولوژی
`Res^B(C_1, C_2) = (A ∨ ~A) →` توتولوژی
مثال ۲:
`C_1: (A B C)`
`C_2: (barA barB D)`
ناسازی روی متغیرهای `A` و `B`.
`Res^A(C_1, C_2) = (B ∨ C ∨ ~B ∨ D) →` ` (B ∨ ~B) →` توتولوژی
■ قضیه پایستاری صدق پذیری واگشایی (Satisfiability Preservation Theorem for Resolution)↧
Mordechai Ben-Ari. Mathematical Logic for Computer Science. 3th, ed, Springer, .2012. 4.24. p 81.
فرض کنید `C` واگشای بندهای `C_۱` و `C_۲` باشد. در این صورت، `C` صدق پذیر است اگر و تنها اگر `C_۱` و `C_۲` هر دو صدق پذیر باشند.
اثبات:
گیریم `C_۱` و `C_۲` تحت تعبیر `cc"I"` صدق پذیر و `l` و `l^c` لیترال باشند.
از آنجا که `l` و `l^c` متمماند، یا `(l)^cc"I" = T` یا `(l^c)^cc"I" = T`.
فرض کنید `(l)^cc"I" = T`. در این صورت:
`(l^c)^cc"I" = F` و `C_۲` (بندی که شامل `l^c` است) تنها وقتی میتواند (تحت تعبیر `I`) صدقپذیر شود که برای لیترال دیگری مانند `l'` (بقسمی که `l' ≠ l^c`)، داشته باشیم `(l')^cc"I" = T`. بنابر ساخت قاعدهٔ واگشایی، `l' ∈ C`، پس `cc"I"` نیز مدلی برای `C` است. استدلالی متقارن آنچه آمد در صورتی برقرار است که `(l^c)^cc"I" = T`.
برعکس، گیریم `cc"I"` تعبیری باشد که `C` را صدق پذیر میکند.
پس `(l')^cc"I" = T` برای دستکم یک لیترال `l' ∈ C` برقرار است. طبق قاعدهٔ واگشایی، `l' ∈ C_۱` یا `l' ∈ C_۲` (یا هر دو) است.
اگر `l' ∈ C_۱`، آنگاه `Value(C_۱)^cc"I" = T`. از آنجا که نه `l in C` و نه `l^c in C` ، پس `cc"I"` روی `l` و هم `l^c` تعریف نشده است، و میتوانیم `cc"I"` را با تعریف `(l^c)^cc"I"' = T` به تعبیری `cc"I"'` بگسترانیم. چون `l^c in C_۲`، داریم :
`Value(C_۲)^{cc"I"'} = T` و `Value(C_۱)^{cc"I"'} = Value(C_۱)^cc"I" = T`
(زیرا `cc"I"'` گسترشی از `cc"I"` است)، پس `cc"I"'` مدلی برای `C_۱` و هم `C_۲` است. استدلال متقارن در صورتی برقرار است که `l' ∈ C_۲`.
■ افراز مجموعه متناهی بندوارهها (قاعده جدایش `p` / `p`-Separation)
فرض کنید `S` یک مجموعه متناهی ار بندواره باشد. برای هر حرف گزارهای `p` قرارداد میکنیم که:
⏺ `S_p^+` مجموعه بندوارههایی از `S` باشد که شامل لیترال `p` باشند (به صورت `p vv A`).
⏺ `S_p^-` مجموعه بندوارههایی از `S` باشد که شامل لیترال `~p` باشند (به صورت `p vv B`).
⏺ `S_0` مجموعه بندوارههایی از `S` باشد که شامل نه `p` و نه `~p` باشند.
فرض کنید `R_p` مجموعه تمام واگشاها روی `p` باشد که با واگشایی هر بندواره در `S_p^+` با هر بندواره در `S_p^−` به دست میآید؛ یعنی:
`R_p={A vv B| (p vv A)∈S_p^+,(~p vv B)∈S_p^−}.`
مجموعه `R_p` را افراز `p` مجموعه `S` مینامیم. اکنون مجموعه `S^'` را از قرار زیر تعریف میکنیم:
`S^' = S_0 cup R_p`.
و آن را قاعده جدایش p (p-separation) (یا بطور کوتاه قاعده واگشایی) مجموعه `S` مینامیم.
بنا به قضیه پایستاری صدق پذیری واگشایی برای هر حرف گزارهای داریم:
`S` صدقپذیر است `Leftrightarrow^` `S^'` صدقپذیر است،
که در آن `S'` عبارت از جدایش `p` (p-separation) مجموعه `S` است
■ فراروند واگشایی (Resolution procedure)
فراروند واگشایی منطقی، که در ادامه خواهیم دید، رویهای استوار با تمامیت وازنشی برای آزمون صدق ناپذیری مجموعهای متناهی از فرمولها است که با تمرکز بر یک قاعده استنتاج واحد و قدرتمند (قاعده واگشایی)، از سیستمهای سنتی (مانند استنتاج طبیعی) متمایز میشود.
فراروند واگشایی چرخهوار قاعده واگشایی را روی جفت بندوارهها بکار میبرد، بندوارههای جدیدی تولید میکند و آنها را به مجموعه میافزاید. روند زمانی بازمیایستد که بندواره تهی (`bot`) دستآمده شود یا جفت بندوارهای یافته نشود. دستآمدن `bot` نشان میدهد که یک تناقض پیدا شده است. که این یعنی، مجموعه اولیه بندوارهها صدق ناپذیر است. در غیر این صورت مجموعه صدق پذیر است.
ما در اینجا، شرح الگوریتم واگشایی را از یک سطح کلیتر (بالاتر) آغازمیکنیم، جایی که با بندوارهها به شکل گستردهترشان روبرو میشویم و به ساختار کلی روابط منطقی آنها توجه میکنیم. از این منظر کلی، الگوریتم به تدریج به سطوح جزئیتر (پایینتر) پیش خواهد رفت، جایی که توجه به لیترالهای خاص درون بندوارهها معطوف میشود. در هر مرحله، این لیترالها و روابط بین آنها سیستماتیک واگشایی میشوند، به طوری که فرآیند از یک دیدگاه گسترده و انتزاعی از مسئله به سمت عملیات منطقی به طور فزایندهای دقیقتر پیش میرود. این سازماندهی بالا به پایین، با ترسیم یک چارچوب منطقی کلی و سپس پالایش آن از طریق جزئیسازی تدریجی، به هدایت کارآمد مسیر کمک میکند.
■ الگوریتم واگشایی (Resolution algorithm)
الگوریتم- (فراروند واگشایی)↧
Mordechai Ben-Ari. Mathematical Logic for Computer Science. 3th, ed, Springer, .2012. 4.18. p 81.
ورودی: مجموعه متناهی `S` از بندوارهها
خروجی: صدق پذیری یا صدق ناپذیری `S`
۱. `S_0 leftarrow S` // مجموعه خالی `S_0` را از عناصر `S` پر میکنیم.
۲. چرخه گامهای زیر را برای بدست آوردن `S_{i+1}` از `S_i` تا وقتی فراروند پایان نیابد تکرار میکنیم:
۲.۱ جفت بندوارههای ناسازه `C_1` و `C_2` را بقسمیکه `{C_1،C_2} ⊆ S_i` و پیشتر انتخاب نشده باشند، انتخاب میکنیم.
۲.۲ `C`، یعنی واگشا، را از قرار `C leftarrow Res(C_1, C_2)` مطابق قاعده واگشایی حساب میکنیم.
۲.۳ اگر `C` یک بندواره بدیهی نیست:
`S_{i+1}` را `S_i ∪ {C}` بگیرید (`S_{i+1} leftarrow S_i ∪ {C}`)؛
در غیر این صورت:
`S_{i+1}` را از قرار `S_i` بگیرید (`S_{i+1} leftarrow S_i`).
۲.۴ اگر `C = bot` فراروند را پایان دهید. // `S` ناسازگار (صدق ناپذیر) است.
۲.۵ اگر تمام جفت بندوارههای ناسازه واگشایی شدهاند فراروند را پایان دهید. // `S` صدق پذیر) است.
// با توجه به متناهی بودن `S` این الگوریتم در یکی از دستورهای ۲.۴ یا ۲.۵ پایان مییابد.
■ کدواره الگوریتم واگشایی (Pseudocode of the resolution algorithm)
Algorithm: Resolution
Input: S (S یک مجموعه متناهی بندواره است.)
Output: "صدقناپذیر" یا "صدقپذیر"
Procedure Resolution(S):
`S_0 ← S`
`i ← 0`
resolved_pairs ← `O/`
// مجموعه resolved_pairs جفت بندوارههای انتخابشده تا کنون را ذخیره میکند.
repeat
// چرخه انتخاب جفت بندوارههای مجموعه `S_i` که باهم در تقابل هستند.
pair_found ← false
for each unordered pair `{C_1, C_2}sube S_i` do
if `{C1, C2}!in`resolved_pairs and Opposing`(C1, C2)` then
// نشان گذاری این دوگانه به عنوان انتخاب شده:
resolved_pairs← resolved_pairs`cup``{{C1`, `C2}}`
// محاسبه واگشا(resolvent):
`C ←``Res(C1, C2)`
// شرط پایان ۱: بندواره تهی دست آمده است؟
if `C = bot` then
return "unsatisfiable"
end if
// بهروزرسانی `S_{i+1}` بر این اساس که `C` بدیهی است یا نه؟
if IsTrivial`(C)` then
`S_{i+1} ← S_i`
else
`S_{i+1} ← S_i cup {C}`
end if
pair_found ← true
`i ← i + 1`
// پرش به چرخه بعد با `S_i` جدید:
break
end if
// شرط پایان ۲: همه دوگانههای ناسازه واگشایی شدهاند؟
if not pair_found then
return "satisfiable"
end if
end for
until false
End Procedure
۱- تابع کمکی برای تعیین ناسازگی بندوارهها:
Function Opposing(`C1`, `C2`):
// این تابع در صورتی که `C1` و `C2` دارای لیترالهای متمم باشند، مقدار true بازمیگرداند.
for each literal `ℓ``in``C1` do
// چرخه دستیابی به لیترالهای `C1`.
if ~`ℓ``in``C2` then
return true
end if
end for
return false
End Function
۲- تابع کمکی برای محاسبه واگشا (Resolvent):
Function Res(`C1`, `C2`):
// محاسبه واگشای `C1` و :`C2`
for each literal `ℓ``in``C1` do
// چرخه دستیابی به لیترالهای `C1`.
if ~`ℓ``in``C2` then
return `(C1 - {ℓ})``cup``(C2 - {~ℓ})`
end if
end for
return false
End Function
۳- تابع کمکی برای تعیین بدیهی بودن بودن بندواره:
Function Opposing(`C`):
// این تابع در صورتی که `C1` بدیهی باشند، مقدار true برمیگرداند.
for each literal `ℓ``in``C` do
if ~`ℓ``in``C` then
return true
end if
end for
return false
End Function
■ مثال برای فراروند واگشایی
مثال ۱:
| با کارزدن فراروند واگشایی نشان میدهیم صورت استدلالی سمت چپ معتبر است. | ۱. `(r => u)` ۲. `(u => ~ w)` ۳. `r` `∴ ~ w` | ||
  | ابتدا مقدمات و نقیض نتیجه را به صورت بندوارهای برمیگردانیم: | ||
| مقدمه ۱ | `{bar r u}` | ۱. | |
| مقدمه ۲ | `{bar u bar w}` | ۲. | |
| مقدمه ۳ | `{r}` | ۳. | |
| نقیض نتیجه | `:. ~( ~ w) ≡ {w}` | ۴. | |
| صورت بندوارهای: ۱، ۲، ۳ و ۴ | `{color(red)(bar r) u , bar u bar w, color(red)r, w}` | ۱'. | |
| '۱ و واگشایی روی `r` | `{color(red)u, color(red)(bar u) bar w, w}` | ۲'. | |
| '۲ و واگشایی روی `u` | `{bar w, w}` | ۳'. | |
| '۳ و واگشایی روی `w` | `color(red)(bot)` | ۴'. | |
مثال ۲:
با کارزدن فراروند واگشایی نشان میدهیم مجموعه فرمول `S` از قرار:
`S = {p, ~p vv q, ~r, ~p vv ~q vv r }` `⇆` `S = {p, bar p q, bar r, bar p bar q r}`
یک مجموعه فرمول ناسازگار است.
  | ||
| `p in S` | `p` | ۱. |
| `bar p q in S` | `bar p q` | ۲. |
| `bar r in S` | `bar r` | ۳. |
| `bar p bar q r in S` | `bar p bar q r` | ۴. |
| ۳ و ۴ | `bar p bar q` | ۵. |
| ۵ و ۲ | `bar p` | ۶. |
| ۱ و ۶ | `color(red)(bot)` | ۷. |
مثال ۳:
با کارزدن فراروند واگشایی نشان میدهیم مجموعه فرمول `S` از قرار:
`{C_۱: p, C_۲: bar p q r, C_۳: bar p bar q bar r, C_۴: bar p s t, ``C_۵: bar p bar s bar t, C_۶: bar s q, C_۷: r t, C_۸: bar t s}`
یک مجموعه فرمول ناسازگار است.
`{C_۱: p, ``C_۲: bar p q r, ``C_۳: bar p bar q bar r, ``C_۴: bar p s t, ``C_۵: bar p bar s bar t, ``C_۶: bar s q, ``C_۷: r t, ``C_۸: bar t s}`
■ آزمایشگاه منطق: الگوریتم واگشایی (Resolution Algorithm)
آزمایشگاه
الگوریتم واگشایی (Resolution algorithm)
برای ورود به آزمایشگاه الگوریتم واگشایی روی دکمه
کلیک کنید.
■ استواری روش واگشایی (The soundness of resolution method)
قضیه: فراروند واگشایی استوار (Sound) است. یعنی اگر با فراروند واگشایی از مجموعه بندوارههای `S` بندواره تهی (`bot`) بدست آید، آنگاه `S` صدق پذیر نیست. به عبارت دیگر:
اگر `S` `vdash``Res``bot`، آنگاه `S` صدق پذیر نیست. [فراقضیه استواری]
اثبات:
۱: فرض خلاف:
گیریم روش واگشایی استوار (Sound) نیست. این یعنی مجموعه بندوارهها `S` هست، بقسی که:
آ- `S vdash_{Res} bot`. ب- `S` صدق پذیر است.
۲:
فرض کنید دنباله حاصل از فراروند واگشایی دنباله متناهی از بندوارههای `C_۱, C_۲, ..., C_n` باشد، که در آن `C_n` بندواره تهی (`bot`) است. (برای مثال دنباله
`C_۱=p, C_۲ = bar{p}q, C_۳ = bar r , C_۴=bar{p}bar{q}r ,``C_۵=bar{p}bar{q}, C_۶ = bar p, C_۷ =bot`
در مثال ۲ در بالا ).
هر بندواره `C_i` در این دنباله یکی از موردهای زیر است:
• یک بندواره در مجموعه اصلی `S`.
• واگشای (Resolvent) دو بندواره قبلی `C_j` و `C_k` در دنباله (که در آن `j, k lt i`) است.
میتوانیم این روند را به صورت مجموعهای از بندوارههای در حال گسترش نمایش دهیم:
• فرض کنید `S_۰ = S`.
• فرض کنید `S_۱ = S_۰ ∪ {C_۱}`، که در آن `C_۱` اولین دستآمده از واگشا است.
• فرض کنید `S_۲ = S_۳ ∪ {C_۲}`، که در آن `C_۲` دومین دستآمده از واگشا است.
• ... و به همین ترتیب، تا ... `S_n = S_{n₋۱} ∪ {C_n}`، که در آن `C_n = bot`. مجموعه پایانی `S cup {C_۱, C_۲, ..., bot}` خواهد بود.
۳:
• طبق فرض خلف در بند ۱، مجموعه `S_۰ = S` صدقپذیر است.
• اکنون `S_۱ = S_۰ ∪ {C_۱}` را در نظر بگیرید. از آنجایی که `C_۱` توسط قاعده واگشایی از بندهای `S_۰` دست آمده است، بنا بر قضیه پایستاری صدق اگر `S_۰` صدق پذیر باشد، پس `S_۱` نیز باید صدق پذیر باشد.
• سپس، `S_۲ = S_۱ ∪ {C_۲}` را در نظر بگیرید. با همین منطق، از آنجایی که `C_۲` از بندهای `S_۱` دست آمده است و نشان دادیم که `S_₁` صدق پذیر است، قضیه پایستاری تضمین میکند که `S_۲` نیز صدق پذیر است.
• این روند را برای هر مرحله از دستآوری (derivation) ادامه میدهیم. در هر مرحله `i`، مجموعه `S_i` صدق پذیر است. بنا به استقرا، مجموعه پایانی در دنباله، `S_n`، نیز باید صدق پذیر باشد.
۴.
• بنابراین طبق منطق بالا، مجموعه پایانی `S_n = S cup {C_۱, C_۲, ..., bot}` باید صدق پذیر باشد.
• اما `S_n` شامل بندواره تهی (`bot`) است که صدق پذیر نیست.
• هر مجموعهای از بندوارهها که شامل یک بندواره صدقناپذیر (در این مورد، `bot`)، خود نیز صدقناپذیر است. بنابراین، `S_n` نیز باید صدقناپذیر باشد.
۵:
• از مرحله ۳، نتیجه گرفتیم که مجموعه `S_n` باید صدقپذیر باشد.
• از مرحله ۴، نتیجه گرفتیم که مجموعه `S_n` باید صدقناپذیر باشد.
بنا بر این تناقض، فرض خلاف (اینکه یک مجموعه صدقپذیر `S` میتواند منجر به دست آوردن `bot` شود) نادرست است.
■ تمامیت وازنشی واگشایی در منطق گزارهای (Resolution Refutation Completeness)
قضیه:
اگر مجموعهای متناهی از بندوارهها، `S`، تصدیقناپذیر باشند، آنگاه کارزدن مکرر قاعده واگشایی در نهایت منجر به دست آوری بندواره تهی (`bot`) خواهد شد. بگونه همارز: قاعده واگشایی در منطق گزارهای دارای تمامیت وازنشی است.
اثبات:
فرض کنید `n` تعداد متغیرهای گزارهای متمایزی باشد که در `S` رخ میدهند. ما با استقرا روی `n` نشان میدهیم اگر `S` صدقناپذیر باشد، آنگاه میتوان با حذف پیدرپی متغیرها (واگشایی)، بندواره تهی را به دست آورد.
گام پایه: `n=0`:
اگر در `S` متغیری وجود نداشته باشد، هر بندواره یک بندواره تهی `bot` (صدقناپذیر) یا یک توتولوژی است (دومی نمیتواند بدون متغیرها وجود داشته باشد). بنابراین اگر `S` صدقپذیر نباشد، از قبل شامل `bot` است، بنابراین بندواره تهی قابل استخراج است.
گام استقرایی:
فرض کنید قضیه برای همه مجموعه بندوارههایی که تعداد متغیرهای آنها کمتر از `n` است برقرار است. `S` را با `n` متغیر در نظر بگیرید و فرض کنید `S` صدقناپذیر است. متغیر `p` را که در `S` روی داده انتخاب کنید و صورتبندی "حذف `p`" ، همانطور که در بالا گفته شد، را تشکیل دهید، یعنی `S′ = S_0∪R_p` .
`S′` (طبق لم،) صدقناپذیر است (زیرا صدقپذیری `S` و `S′` باهم است). مجموعه `S′` شامل متغیرهای گزارهای اکیداً کمتری نسبت به `S` است (متغیر `p` دیگر در `S′` نخواهد بود).
بنا بر فرض استقرا، واگشایی کامل روی متغیرهای ′S′ منجر به بندواره تهی میشود.
اما واگشاهای (resolvents) موجود در `S′` با واگشایی بندهای `S` روی `p` به دست آمدهاند و واگشاییهای بیشتر که بندواره تهی را تولید میکنند را میتوان با مراحل واگشایی روی بندوارههایی که از `S` سرچشمه میگیرند، شبیهسازی کرد.
بنابراین، بندواره تهی با کارزدن چرخهای قاعده واگشایی از `S` قابل استخراج است. این استقرا را کامل میکند.
■ کارآمدی الگوریتم واگشایی (Resolution algorithm efficiency)
ما نشان دادیم که فراروند واگشایی دارای تمامیت وازنشی است. این بدان معناست که اگر مجموعهای از بندوارهها ناسازه باشند، واگشایی سرانجام به یک تناقض (بندواره خالی، `bot`) خواهد رسید. با این حال، فراروند واگشایی اگرچه یک روند کارآمد است ولی کارسازی (سرعت اجرای درخور) را تضمین نمیکند.
چالش اساسی الگوریتم واگشایی، پتانسیل "انفجار" در تعداد بندوارهها است. به یاد بیاورید که این الگوریتم با تولید بندوارههای جدید (واگشا) از جفت بندوارههای موجود کار میکند. در بدترین حالت، حل مجموعهای از بندوارهها میتواند تعدادی بندواره جدید ایجاد کند که به صورت نمایی نسبت به اندازه ورودی رشد میکنند. در واقع در رده مسئلههای سخت در منطق و علوم کامپیوتر جای میگیرد. در ادامه این بند به قاعده واگشایی که هسته الگوریتم واگشایی است و کارآمدی آن متمرکز خواهیم شد.
■ کارآمدی قاعده جدایش (Efficiency of the Separation Rule)
پیشتر قاعده واگشایی را معرفی کردیم. بنابراین میتوان نوشت:
`R_p =A vv B∣(p vv A) in S_{+p}, (~p vv B) in S_p}`.
و همنجا مجموعه `S'` را به قرار زیر:
`S′ =S_0 ∪ R_p` ↜,
تعریف کردیم. میتوان دید که `S'` با واگشایی متغیر `p` از `S` به دست میآید. این یعنی: هر مدل `S` که به متغیرهای باقیمانده محدود شده باشد، مدل `S'` نیز هست و نیز وارون آن. همچنین قضیه پایستاری صدق پذیری واگشایی، تضمین میکند که `S` صدق پذیر است، اگر `S'` صدق پذیر باشد.
ما در ادامه این بند به کارآمدی قاعده واگشایی و تأثیرات مثبت و منفی آن بر کارآمدی اجرای الگوریتم واگشایی میپردازیم.
۱. واگشایی محلی در مقابل واگشایی سرتاسری
الگوریتم واگشایی، که پیشتر معرفی شد به شیوه چرخهای محاسبات را انجام میدهد. یعنی:
۱- یک جفت از بندوارههایی را انتخاب میکند که حاوی لیترالهای متمم هستند.
۲- واگشای آنها را حساب میکند.
۳- واگشا را به مجموعه بندوارهها میافزاید و سپس چرخه بعدی.
این منجر به دو منبع اصلی ناکارآمدی میشود:
۱- معمولاً در هر چرخه جفتهای متمم زیادی از بندوارهها برای واگشایی وجود دارد.
۲- ممعمولاً متغیرهای زیادی وجود دارند که میتوان بر اساس آنها تصمیمگیری کرد.
در مقابل، قاعده جدایش بر روی یک متغیر واحد `p` تمرکز میکند و تمام راهحلهایی را که `p`s را جدا میکنند، در یک مرحله سیستماتیک انجام میدهد:
• به جای پرسیدن «کدام دو بندواره را باید در مرحله بعد واگشایی کنیم؟»،
• میپرسیم «چه میشود اگر `p` را به طور کامل از `S` حذف کنم؟».
این نکته وجه جستجو را کاهش میدهد، زیرا با انتخاب متغیر p، قاعده خود دقیقاً واگشاهای تولیدی (موجود در `R_p`) را تعیین میکند. از وجه پیادهسازی، این رویکرد قطعیتر و ساختاریافتهتر (نسبت به واگشاهای دلخواه) است.
۲. رشد تعداد بندوارهها و هزینه اصلی
• تعداد بندوارههایی که `p` در آنها روی داده است: `abs(S+p)=m`
• تعداد بندوارههایی که `~p` در آنها روی داده است: `abs(S-p)=n`
بنابراین در بدترین حالت، قاعده واگشایی ممکن است تا
`abs(R_p) <= m.n`
بندواره جدید ایجاد کند. از قرار یک بندواره برای هر جفت زیر:
`(p vvA) in S+p` و `(¬p vv B) in S−p`.
همزمان، این قاعده تمام بندوارههایی که شامل `p` یا `¬p` هستند را حذف میکند؛ یعنی `m+n` بندواره را حذف کرده و حداکثر `m . n` واگشا اضافه میکند.
بنابراین:
• اگر `m` و `n` هر دو کوچک باشند، تعداد بندوارههای جدید نیز کم است و حذف `p` میتواند مسئله را کوچکتر کند یا تقریباً اندازه آن را ثابت نگه دارد.
• اگر `m` و `n` بزرگ باشند، `m . n` میتواند بسیار بزرگتر از `m+n` باشد.
در چنین مواردی، حذف `p` میتواند مجموعه بندوارهها را بسیار بزرگ و اداره نشدنی کند و مسئله را بزرگتر و سختتر کند.
این بدهبستان اصلی در کارایی قاعده واگشایی است: میتواند مجموعه بندوارهها را به طرز چشمگیری ساده کند یا اندازه آن را به شدت افزایش دهد، بسته به اینکه `p` چند بار اتفاق میافتد.
۳. روشهای میانبر (Heuristics) برای انتخاب یک متغیر واگشایی مناسب
به دلیل انفجار احتمالی بندوارهها، الگوریتمهای عملی به ندرت متغیرها را با ترتیب ثابت یا دلخواه حذف (جدا) میکنند. آنها از روشهای میانبر (Heuristics) برای انتخاب «بهترین» متغیر برای واگشایی بعدی استفاده میکنند. برخی ایدههای معمول عبارتند از:
• روش میانبر فراوانی (Frequency heuristic):
متغیری انتخاب میشود که برای آن هر دو متغیر `m=|S+p|` و `n=|S−p|` کوچک باشند. این کار `|R_p| ≤ m.n` را تحت کنترل نگه میدارد.
• روش میانبر متوازن ( Balance heuristic):
متغیرهایی که فقط به صورت مثبت یا فقط به صورت منفی `(m=0 یا n=0)` رخ میدهند (یعنی به صورت اتم یا نقیض اتم)، حذف آنها ارزان است، زیرا در این صورت `R_p=O/` و ما به سادگی تمام بندهای حاوی `p` یا `¬p` را حذف میکنیم.
اگر `p` فقط به صورت `p` ظاهر شود (هرگز به صورت `¬p` نباشد)، آنگاه هیچ جفت جملهای به شکل `(p∨A)` و `(¬p∨B)` وجود نخواهد داشت. بنابراین `S-p` خالی است، `R-p=O/`، و حذف `p` هیچ جمله جدیدی اضافه نمیکند. به طور مشابه، اگر `p` فقط به صورت `¬p` ظاهر شود، `S+p` خالی است و دوباره هیچ حلکنندهای ایجاد نمیشود. از همین جهت گفته میشود حذف چنین متغیرهایی «ارزان» یا «ایمن» است: آنها باعث افزایش تعداد واگشاها در `m.n` نمیشوند.
۴. دیدگاه پیچیدگی
از دیدگاه نظری:
• هر روش استدلال گزارهای که دارای تمامیت است (از جمله روشهای مبتنی بر واگشایی) باید در بدترین حالت، از زمانی استفاده کند که از نظر تعداد متغیرها نمایی باشد. این امر از این واقعیت ناشی میشود که این مسئلهها در رده NP-کامل (NP-complete) جای دارند.
• قاعده واگشایی این پیچیدگی بدترین حالت را تغییر نمیدهد. اما، میتواند:
• بسیاری از نمونهها را در عمل را تا حد زیادی ساده کند، و
• یک ساختار الگوریتمی واضح ارائه دهد که پیادهسازی و استدلال در مورد آن آسان باشد.
افزون بر آن
برای آموزشی و تحلیل ارزشمند است. چرا که:
۱. ارتباط بین واگشایی و واگشایی را آشکار کند.
۲. پلی به رویههای پیشرفتهتر که به روشهای میانبری حذف، تقسیم و جستجو متکی هستند، فراهم میکند.
به طور خلاصه، قاعده واگشایی تا آن اندازه کارساز است که بتوانیم:
• متغیرهای واگشایی را حساب شده انتخاب کنیم، و
• رشد مجموعه بندوارهها را همراه پیستاری صدق پذیری مدیریت کنیم.
مراجع:
1- Guo, W., et al. Machine Learning Methods in Solving the Boolean Satisfiability Problem. 2022. arXiv:2203.04755, https://doi.org/10.48550/arXiv.2203.04755..
2- Biere, Armin., et al (Eds.). Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 2009.
3- Cook, S. A. The Complexity of Theorem-Proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC), Association for Computing Machinery, 1971, pp. 151–158.
شماره ۳ یک مقاله بنیادی است که نشان داد SAT یک مسئله NP-کامل است و پایه نظریه پیچیدگی رایانشی را بنا نهاد.
این روشهای اکتشافی در الگوریتم دیویس-پاتنام و الگوریتمهای مرتبط ظاهر میشوند، که در آنها اعمال مکرر قاعده جدایش (حذف متغیر) با تقسیم و عقبگرد دنبال میشود (به بخش SAT در زیر مراجعه کنید).
■ ■ ■ ■ ■
 |  |