ارضاپذیری هورن

در منطق صوری ارضا پذیری هورن عبارت است از مسئلهٔ تعیین اینکه آیا مجموعهٔ مفروضی از عبارتهای هورن گزاره ای ارضا پذیر است یا نه. یک عبارت هورن عبارتی با حداکثر یک لفظ مثبت که سر عبارت نامیده می‌شود و هر تعدادی لفظهای منفی که بدنهٔ عبارت را تشکیل می‌دهد .

یک فرمول هورن یک فرمول گزاره ایست که به وسیلهٔ پیوند دادن عبارت‌های هورن شکل یافته است.

مسألهٔ ارضا پذیری هورن در زمان چند جمله ای قابل حل است. یک الگوریتم زمان چند جمله ای برای ارضا پذیری هورن متکی بر قاعدهٔ انتشار واحد است. اگر فرمول شامل یک عبارت مرکب از یک لفظ تک $l$ (یک عبارت واحد) باشد آنگاه همهٔ عبارتهای شامل $l$ حذف می‌شوند و در همهٔ عبارتهای شامل $\neg l$ نیز این لفظ حذف می‌شود، نتیجهٔ قاعدهٔ دوم ممکن است خود یک عبارت واحد باشد که به همین شیوه انتشار می‌یابد. فرمول ارضا پذیر است اگر این تغییرات موجب ایجاد یک زوج عبارت‌های واحد مخالف $l$ و $\neg l$ نشود.

ارضا پذیری هورن عملاٌ یکی از "سخت ترین" یا " بیان کننده ترین" مسائلی است که می دانیم در زمان چند جمله ای قابل حل است، به این مفهوم که یک مسئلهٔ پ-کامل(P-copmlete) است. این الگوریتم همچنین امکان تعیین انتصاب صدق به فرمول‌ها فرم ارضا پذیر می‌دهد : به همهٔ متغیرهای موجود در یک عبارت واحد مقداری داده می‌شود که آن عبارت واحد را ارضا کند. همهٔ لفظ‌های دیگر کاذب شمرده می‌شوند. انتصاب حاصل یک مدل حداقل فرمول هورن است یعنی در این انتصاب مجموعهٔ حداقلی متغیرها صدق نسبت داده شده و در آن، مقایسه با استفاده از گنجاندن در مجموعه انجام می‌شود.

با استفاده از الگوریتم خطی برای انتشار واحد الگوریتم در اندازهٔ فرمول خطی است.

منطقی است که بپرسیم آیا می‌توان با تبدیل هر مسئلهٔ SAT به Horn_SAT و سپس حل آن در زمان چند جمله ای، Horn_SAT را برای اثبات NP = P به کار برد؟ مسئله اینجا دو جنبه دارد : اول اینکه تبدیل مسئلهٔ SAT به Horn_SAT زمان نمایی لازم دارد و دوم اینکه تبدیل حاصل از حیث طول نمایی است . تأمیم طبقهٔ فرمول‌های هورن، تأمیم فرمول‌های نام گذاری پذیر هورن هستند که عبارت است از مجموعه فرمول هایی که می‌توان با جایگزین کردن برخی از متغیر با منفیِ مربوطهٔ آنها در شکل هورن جای داد. بررسیِ وجودِ چنین جایگزینی ای می‌تواند در زمان خطی انجام شود، بنابراین ارضاپذیریِ اینگونه فرمول هادر P است که می‌توان آن را چنین حل کرد که نخست این جابجایی را انجام داد و سپس ارضاپذیری فرمول هورنِ حاصل را کنترل کرد.

منابع

English Wikipedia : Horn_satisfiability