صدق‌پذیری هورن

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

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

مسئلهٔ ارضاپذیری هورن در زمان چندجمله‌ای قابل حل است. یک الگوریتم زمان چندجمله‌ای برای ارضاپذیری هورن متکی بر قاعدهٔ انتشار واحد است. اگر فرمول شامل یک عبارت مرکب از یک لفظ تک ${\displaystyle l}$

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

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

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