برنامج حل مسألة الاستيفاء (SAT) هو برنامج حاسوبي يهدف إلى حل مسألة الاستيفاء المنطقي. فعند إدخال صيغة رياضية تتضمن متغيرات منطقية مثل (x أو y) و(x أو ليس y)، يتمثل دور برنامج حلّ مسألة الاستيفاء المنطقي في التحقق مما إذا كانت هذه الصيغة قابلة للاستيفاء، أي أن هناك قيمًا ممكنة لـ x وy تجعل الصيغة صحيحة، أو غير قابلة للاستيفاء، أي أنه لا توجد مثل هذه القيم لـ x وy. في هذه الحالة، تكون الصيغة قابلة للاستيفاء عندما تكون x صحيحة، لذا يجب أن يُجيب البرنامج بأن الصيغة "قابلة للاستيفاء". منذ ظهور خوارزميات حلّ مسألة الاستيفاء المنطقي في ستينيات القرن الماضي، تطورت برامج حلّ هذه المسألة الحديثة لتصبح برامج معقدة تتضمن عددًا كبيرًا من الطرق الاستدلالية وتحسينات البرامج لضمان كفاءة عملها.
تُعدّ مسألة استيفاء الصيغ المنطقية، وفقًا لنظرية كوك-ليفين، مسألةً كاملةً من فئة كثيرات الحدود غير القطعية بشكل عام. ونتيجةً لذلك، لا تُعرف سوى خوارزميات ذات تعقيد أسي في أسوأ الحالات. وعلى الرغم من ذلك، فقد طُوّرت خوارزميات فعّالة وقابلة للتوسع لمسألة استيفاء الصيغ المنطقية خلال العقد الأول من الألفية الثانية، مما ساهم في تحقيق تقدّم هائل في القدرة على حلّ مسائل تتضمن عشرات الآلاف من المتغيرات وملايين القيود تلقائيًا.
غالبًا ما تبدأ خوارزميات حلّ مسألة استيفاء الصيغ المنطقية بتحويل الصيغة إلى صيغة الاقتران المعيارية. وتعتمد هذه الخوارزميات عادةً على خوارزميات أساسية مثل خوارزمية ديفيس-بوتنام-لوفلاند، ولكنها تتضمن عددًا من الإضافات والميزات. تتضمن معظم خوارزميات حلّ مسألة استيفاء الصيغ المنطقية مهلة زمنية، بحيث تتوقف في وقت معقول حتى لو لم تتمكن من إيجاد حلّ، مع إخراج نتائج مثل "غير معروف" في الحالة الأخيرة. غالبًا ما لا تكتفي برامج حل مسائل الاستيفاء بتقديم الإجابة، بل توفر معلومات إضافية، بما في ذلك مثال على التعيين (قيم x و y، إلخ) في حال كانت الصيغة قابلة للحل، أو الحد الأدنى من الشروط غير القابلة للحل في حال كانت الصيغة غير قابلة للحل.
كان لبرامج حل مسائل استيفاء الصيغ المنطقية الحديثة أثرٌ بالغٌ في مجالاتٍ عديدة، منها التحقق من البرمجيات، وتحليل البرامج، ومسائل استيفاء القيود، والذكاء الاصطناعي، وأتمتة التصميم الإلكتروني، وبحوث العمليات. وتتوفر هذه البرامج القوية بسهولة كبرامج مجانية ومفتوحة المصدر، كما أنها مُدمجة في بعض لغات البرمجة، مثل عرض برامج حل مسائل الاستيفاء كقيود في برمجة منطق القيود.