قابلية الإرضاء وفقًا للنظريات

في علوم الحاسوب والمنطق الرياضي ، تُعرف مسألة قابلية الإرضاء المعياري للنظريات ( SMT ) بأنها تحديد ما إذا كانت صيغة رياضية قابلة للإرضاء . وهي تعميم لمسألة قابلية الإرضاء المنطقية (SAT) لتشمل صيغًا أكثر تعقيدًا تتضمن أعدادًا حقيقية ، وأعدادًا صحيحة ، و/أو هياكل بيانات متنوعة مثل القوائم ، والمصفوفات ، ومتجهات البت ، والسلاسل النصية . ويُشتق الاسم من حقيقة أن هذه التعبيرات تُفسَّر ضمن (بمعيار) نظرية شكلية معينة في منطق الرتبة الأولى مع المساواة (غالبًا ما تمنع المُكمِّمات ). تُعد مُحلِّلات SMT أدوات تهدف إلى حل مسألة SMT لمجموعة فرعية عملية من المدخلات. وقد استُخدمت مُحلِّلات SMT مثل Z3 و cvc5 كعنصر أساسي في مجموعة واسعة من التطبيقات في علوم الحاسوب، بما في ذلك الإثبات الآلي للنظريات ، وتحليل البرامج ، والتحقق من البرامج ، واختبار البرمجيات .

بما أن مسألة إرضاء الدوال المنطقية هي مسألة كاملة من فئة NP ، فإن مسألة SMT عادةً ما تكون صعبة من فئة NP ، وهي غير قابلة للتقرير بالنسبة للعديد من النظريات . يدرس الباحثون النظريات أو مجموعات فرعية من النظريات التي تؤدي إلى مسألة SMT قابلة للتقرير، والتعقيد الحسابي للحالات القابلة للتقرير. غالبًا ما تُنفذ إجراءات القرار الناتجة مباشرةً في برامج حل SMT؛ انظر، على سبيل المثال، قابلية تقرير حساب بريسبرغر . يمكن اعتبار SMT مسألة إرضاء قيود ، وبالتالي منهجًا رسميًا لبرمجة القيود .

المصطلحات والأمثلة

بصورة رسمية، تُعرَّف حالة SMT بأنها صيغة في منطق الرتبة الأولى ، حيث تحمل بعض رموز الدوال والمسندات تفسيرات إضافية، وتتمثل مشكلة SMT في تحديد ما إذا كانت هذه الصيغة قابلة للإرضاء. بعبارة أخرى، تخيل حالة من مشكلة الإرضاء البولياني (SAT) حيث تُستبدل بعض المتغيرات الثنائية بمسندات على مجموعة مناسبة من المتغيرات غير الثنائية. المسند هو دالة ثنائية القيمة لمتغيرات غير ثنائية. ومن أمثلة المسندات المتباينات الخطية (مثلًا، $3x+2y-z\geq 4$ ) أو المعادلات التي تتضمن مصطلحات ورموز وظائف غير مفسرة (مثل، $f(f(u,v),v)=f(u,v)$ أين $f$ هي دالة غير محددة ذات وسيطين). تُصنَّف هذه المسندات وفقًا للنظرية المُخصصة لها. على سبيل المثال، تُقيَّم المتباينات الخطية على المتغيرات الحقيقية باستخدام قواعد نظرية الحساب الخطي الحقيقي ، بينما تُقيَّم المسندات التي تتضمن حدودًا غير مُفسَّرة ورموز دوال باستخدام قواعد نظرية الدوال غير المُفسَّرة مع المساواة (والتي تُسمى أحيانًا النظرية الفارغة ). تشمل النظريات الأخرى نظريات المصفوفات وهياكل القوائم (المفيدة لنمذجة برامج الحاسوب والتحقق منها )، ونظرية متجهات البت (المفيدة في نمذجة تصميمات الأجهزة والتحقق منها ). توجد أيضًا نظريات فرعية: على سبيل المثال، منطق الفرق هو نظرية فرعية من الحساب الخطي حيث تُقيَّد كل متباينة بالشكل التالي: $xy>c$ بالنسبة للمتغيرات $x$ و $y$ وثابت $c$ .

توضح الأمثلة أعلاه استخدام الحساب الخطي للأعداد الصحيحة في المتباينات. ومن الأمثلة الأخرى:

قابلية الإرضاء: تحديد ما إذا $x\vee (y\wedge \neg z)$ قابل للتنفيذ.
الوصول إلى المصفوفة: ابحث عن قيمة للمصفوفة A بحيث يكون A [0] = 5.
الحساب باستخدام المتجهات الثنائية: تحديد ما إذا كان x و y عددين مختلفين مكونين من 3 بتات.
الدوال غير المفسرة: أوجد قيمًا لـ x و y بحيث $f(x)=2$ و $g(x)=3$ .

معظم برامج حل SMT تدعم فقط أجزاء من منطقها خالية من المحددات الكمية .

العلاقة بإثبات النظريات الآلي

يوجد تداخل كبير بين حل مسائل المنطق القياسي (SMT) وإثبات النظريات الآلي (ATP). عمومًا، تركز برامج إثبات النظريات الآلية على دعم منطق الرتبة الأولى الكامل مع المُكمِّمات، بينما تركز برامج حل مسائل المنطق القياسي بشكل أكبر على دعم النظريات المختلفة (رموز المسندات المُفسَّرة). تتفوق برامج إثبات النظريات الآلية في حل المسائل التي تحتوي على الكثير من المُكمِّمات، بينما تُحسِّن برامج حل مسائل المنطق القياسي الأداء في حل المسائل الكبيرة التي لا تحتوي على مُكمِّمات. ^{[ 1 ]} والخط الفاصل بينهما غير واضح لدرجة أن بعض برامج إثبات النظريات الآلية تشارك في SMT-COMP، بينما تشارك بعض برامج حل مسائل المنطق القياسي في CASC . ^{[ 2 ]}

القدرة التعبيرية

تُعدّ حالة SMT تعميمًا لحالة SAT المنطقية ، حيث تُستبدل مجموعات مختلفة من المتغيرات بمسندات من نظريات أساسية متنوعة. توفر صيغ SMT لغة نمذجة أكثر ثراءً بكثير مما هو ممكن مع صيغ SAT المنطقية. على سبيل المثال، تسمح صيغة SMT بنمذجة عمليات مسار البيانات للمعالج الدقيق على مستوى الكلمة بدلاً من مستوى البت.

بالمقارنة، تعتمد برمجة مجموعات الإجابات أيضًا على المسندات (وبشكل أدق، على الجمل الذرية المُشتقة من الصيغ الذرية ). على عكس SMT، لا تحتوي برامج مجموعات الإجابات على مُكمِّمات، ولا يُمكنها التعبير بسهولة عن قيود مثل الحساب الخطي أو منطق الفرق - تُعد برمجة مجموعات الإجابات الأنسب للمسائل المنطقية التي تُختزل إلى النظرية الحرة للدوال غير المُفسَّرة. يُعاني تنفيذ الأعداد الصحيحة ذات 32 بت كمتجهات بت في برمجة مجموعات الإجابات من مُعظم المشاكل نفسها التي واجهتها حلول SMT المبكرة: يصعب استنتاج الهويات "الواضحة" مثل x + y = y + x .

توفر برمجة المنطق المقيد دعمًا للقيود الحسابية الخطية، ولكن ضمن إطار نظري مختلف تمامًا. كما تم توسيع نطاق حلول SMT لحل الصيغ في منطق الرتبة العليا . ^[³^]

أساليب الحل

تضمنت المحاولات المبكرة لحل مسائل SMT ترجمتها إلى مسائل Boolean SAT (على سبيل المثال، يتم ترميز متغير عدد صحيح 32 بت بواسطة 32 متغيرًا أحادي البت بأوزان مناسبة، ويتم استبدال عمليات مستوى الكلمة مثل "الجمع" بعمليات منطقية منخفضة المستوى على البتات) وتمرير هذه الصيغة إلى محلل Boolean SAT. يتميز هذا النهج، الذي يُشار إليه بالنهج الاستباقي (أو معالجة البتات )، بمزاياه: فمن خلال المعالجة المسبقة لصيغة SMT إلى صيغة Boolean SAT مكافئة، يمكن استخدام محللات Boolean SAT الحالية "كما هي" والاستفادة من تحسينات أدائها وقدرتها بمرور الوقت. من ناحية أخرى، فإن فقدان الدلالات عالية المستوى للنظريات الأساسية يعني أن محلل Boolean SAT عليه أن يبذل جهدًا أكبر بكثير من اللازم لاكتشاف الحقائق "البديهية" (مثل $x+y=y+x$ (لجمع الأعداد الصحيحة). أدت هذه الملاحظة إلى تطوير عدد من خوارزميات حل مسائل SMT التي تدمج بشكل وثيق الاستدلال المنطقي لبحث من نوع DPLL مع خوارزميات حل خاصة بالنظرية ( خوارزميات T ) التي تتعامل مع اقترانات (AND) المسندات من نظرية معينة. يُشار إلى هذا النهج باسم النهج الكسول . ^{[ 4 ]}

تُعرف هذه البنية باسم DPLL(T) ^{[ 5 ]} ، وهي تُسند مهمة الاستدلال المنطقي إلى مُحلِّل SAT القائم على DPLL، والذي بدوره يتفاعل مع مُحلِّل نظرية T عبر واجهة مُحدَّدة بدقة. يقتصر دور مُحلِّل النظرية على التحقق من جدوى اقترانات مُسندات النظرية المُمرَّرة إليه من مُحلِّل SAT أثناء استكشافه لمساحة البحث المنطقي للصيغة. ولكن لكي يعمل هذا التكامل بكفاءة، يجب أن يكون مُحلِّل النظرية قادرًا على المشاركة في تحليل الانتشار والتعارض، أي أن يكون قادرًا على استنتاج حقائق جديدة من حقائق مُثبتة، بالإضافة إلى تقديم تفسيرات مُوجزة لعدم الجدوى عند ظهور تعارضات نظرية. بمعنى آخر، يجب أن يكون مُحلِّل النظرية تزايديًا وقابلًا للتراجع .

النظريات القابلة للحسم

يدرس الباحثون النظريات أو مجموعات النظريات الفرعية التي تؤدي إلى مشكلة SMT قابلة للتقرير، والتعقيد الحسابي للحالات القابلة للتقرير. ولأن منطق الرتبة الأولى الكامل قابل للتقرير جزئيًا فقط ، فإن أحد مسارات البحث يسعى إلى إيجاد إجراءات قرار فعالة لأجزاء من منطق الرتبة الأولى، مثل منطق القضايا الفعال . ^{[ 6 ]}

يتضمن خط بحث آخر تطوير نظريات قابلة للتقرير متخصصة ، بما في ذلك الحساب الخطي على الأعداد النسبية والأعداد الصحيحة ، ومتجهات البت ذات العرض الثابت، ^{[ 7 ]} والحساب ذو الفاصلة العائمة (الذي يتم تنفيذه غالبًا في حلول SMT عبر bit-blasting ، أي الاختزال إلى متجهات البت)، ^{[ 8 ]}^{[ 9 ]} والسلاسل ، ^{[ 10 ]} وأنواع البيانات (المشتركة) ، ^{[ 11 ]} والمتتاليات (المستخدمة لنمذجة المصفوفات الديناميكية )، ^{[ 12 ]} والمجموعات والعلاقات المنتهية ، ^[¹³^]^[¹⁴^] ومنطق الفصل ، ^[¹⁵^] والحقول المنتهية ، ^[¹⁶^] والدوال غير المفسرة من بين أمور أخرى.

تُعدّ النظريات الرتيبة المنطقية فئة من النظريات التي تدعم نشر النظريات بكفاءة وتحليل التعارضات، مما يُتيح استخدامها العملي ضمن حلول DPLL(T). ^{[ 17 ]} تدعم النظريات الرتيبة المتغيرات المنطقية فقط (المنطقي هو النوع الوحيد )، وتخضع جميع دوالها ومسنداتها $p$ للبديهية

p(\ldots ,b_{i-1},0,b_{i+1},\ldots )\implies p(\ldots ,b_{i-1},1,b_{i+1},\ldots )

تشمل أمثلة النظريات الرتيبة إمكانية الوصول إلى الرسم البياني ، واكتشاف التصادم للأغلفة المحدبة ، والحد الأدنى من القطع ، ومنطق شجرة الحساب . ^{[ 18 ]} يمكن تفسير كل برنامج Datalog على أنه نظرية رتيبة. ^{[ 19 ]}

SMT للنظريات غير القابلة للتقرير

تدعم معظم مناهج SMT الشائعة النظريات القابلة للتقرير . مع ذلك، لا يمكن نمذجة العديد من الأنظمة الواقعية، مثل الطائرة وسلوكها، إلا باستخدام العمليات الحسابية غير الخطية على الأعداد الحقيقية التي تتضمن دوالًا متسامية . هذه الحقيقة تحفز توسيع نطاق مشكلة SMT لتشمل النظريات غير الخطية، مثل تحديد ما إذا كانت المعادلة التالية قابلة للتحقيق:

{\begin{array}{lr}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\vee b\vee -x^{2}\geq 2.3y)\wedge \left(\neg b\vee y<-34.4\vee \exp(x)>{y \over x}\right)\end{array}}

أين

b\in {\mathbb {B} },x,y\in {\mathbb {R} }.

مع ذلك، فإن هذه المسائل غير قابلة للحل عمومًا. (من جهة أخرى، فإن نظرية الحقول المغلقة الحقيقية ، وبالتالي نظرية الرتبة الأولى الكاملة للأعداد الحقيقية ، قابلة للحل باستخدام حذف المُكمِّمات . ويعود الفضل في ذلك إلى ألفريد تارسكي ). كما أن نظرية الرتبة الأولى للأعداد الطبيعية مع الجمع (وليس الضرب)، والتي تُسمى حساب بريسبرغر ، قابلة للحل أيضًا. وبما أن الضرب بالثوابت يُمكن تنفيذه كعمليات جمع متداخلة، فإن العمليات الحسابية في العديد من برامج الحاسوب يُمكن التعبير عنها باستخدام حساب بريسبرغر، مما ينتج عنه صيغ قابلة للحل.

من أمثلة حلول SMT التي تعالج التركيبات المنطقية لذرات النظرية من النظريات الحسابية غير القابلة للتقرير على الأعداد الحقيقية، ABsolver، ^{[ 20 ]} الذي يستخدم بنية DPLL(T) الكلاسيكية مع حزمة تحسين غير خطية كحل نظرية فرعية (غير مكتملة بالضرورة)، و iSAT ، الذي يعتمد على توحيد حل DPLL SAT ونشر قيود الفترات يسمى خوارزمية iSAT، ^{[ 21 ]} و cvc5 . ^{[ 22 ]}

حلول

يلخص الجدول أدناه بعض ميزات العديد من برامج حل SMT المتاحة. يشير عمود "SMT-LIB" إلى التوافق مع لغة SMT-LIB؛ قد تدعم العديد من الأنظمة التي تحمل علامة "نعم" إصدارات أقدم فقط من SMT-LIB، أو توفر دعمًا جزئيًا فقط للغة. يشير عمود "CVC" إلى دعم لغة CVC . يشير عمود "DIMACS" إلى دعم تنسيق DIMACS .

لا تختلف المشاريع في الميزات والأداء فحسب، بل تختلف أيضًا في مدى جدوى المجتمع المحيط، واهتمامه المستمر بالمشروع، وقدرته على المساهمة في التوثيق والإصلاحات والاختبارات والتحسينات.

منصة			سمات						ملحوظات
اسم	نظام التشغيل	رخصة	مكتبة SMT	CVC	ديماكس	النظريات المدمجة	واجهة برمجة التطبيقات (API)	SMT-COMP
ABsolver	لينكس	رخصة القيادة التجارية	الإصدار 1.2	لا	نعم	الحساب الخطي، الحساب غير الخطي	لغة سي++	لا	يعتمد على DPLL
Alt-Ergo	لينكس ، ماك أو إس ، ويندوز	CeCILL-C (ما يعادل تقريبًا LGPL )	إصدار جزئي v1.2 و v2.0	لا	لا	نظرية الفراغ ، الحساب الخطي للأعداد الصحيحة والنسبية، الحساب غير الخطي، المصفوفات متعددة الأشكال ، أنواع البيانات المعدودة ، رموز التيار المتردد ، متجهات البت ، أنواع بيانات السجلات ، الكميات	أوكاميل	2008	لغة إدخال متعددة الأشكال من الدرجة الأولى على غرار لغة ML، تعتمد على حلّ SAT، وتجمع بين أساليب شبيهة بـ Shostak و Nelson-Oppen للاستدلال modulo النظريات
بارسيلوجيك	لينكس	ملكية خاصة	الإصدار 1.2			نظرية فارغة ، منطق الاختلاف	لغة سي++	2009	إغلاق التطابق القائم على DPLL
سمور	لينكس ، ويندوز	بي إس دي	الإصدار 1.2	لا	لا	المتجهات الثنائية	أوكاميل	2009	برنامج حل SAT
بوليكتور	لينكس	معهد ماساتشوستس للتكنولوجيا	الإصدار 1.2	لا	لا	المتجهات الثنائية ، المصفوفات	ج	2009	برنامج حل SAT
CVC3	لينكس	بي إس دي	الإصدار 1.2	نعم		نظرية الفراغ ، الحساب الخطي، المصفوفات، الصفوف، الأنواع، السجلات، المتجهات الثنائية، الكميات	لغة C / لغة C++	2010	إثبات المخرجات إلى HOL
CVC4	لينكس ، ماك أو إس ، ويندوز ، فري بي إس دي	بي إس دي	نعم	نعم		العمليات الحسابية الخطية للأعداد النسبية والصحيحة، والمصفوفات، والصفوف، والسجلات، وأنواع البيانات الاستقرائية، والمتجهات الثنائية، والسلاسل النصية، والمساواة على رموز الدوال غير المفسرة.	لغة سي++	2021	تم إصدار النسخة 1.8 في مايو 2021
cvc5	لينكس ، ماك أو إس ، ويندوز	بي إس دي	نعم	نعم		العمليات الحسابية الخطية للأعداد النسبية والصحيحة، والمصفوفات، والصفوف، والسجلات، وأنواع البيانات الاستقرائية، والمتجهات الثنائية، والحقول المنتهية، والسلاسل النصية، والمتتاليات، والحقائب، والمساواة على رموز الدوال غير المفسرة.	سي++، بايثون، جافا	2021	تم إصدار النسخة 1.0 في أبريل 2022
مجموعة أدوات إجراءات اتخاذ القرار (DPT)	لينكس	أباتشي	لا				أوكاميل	لا	يعتمد على DPLL
iSAT	لينكس	ملكية خاصة	لا			الحساب غير الخطي		لا	يعتمد على DPLL
اختبار الرياضيات	لينكس ، ماك أو إس ، ويندوز	ملكية خاصة	نعم		نعم	نظرية الفراغ ، الحساب الخطي، الحساب غير الخطي، المتجهات الثنائية، المصفوفات	لغات البرمجة : C / C++ ، بايثون ، جافا	2010	يعتمد على DPLL
ميني سمت	لينكس	إل جي بي إل	جزئي الإصدار 2.0			الحساب غير الخطي	أوكاميل	2010	يعتمد على حل SAT، ويعتمد على Yices
نورن									برنامج حل قيود السلاسل النصية (SMT)
أوبن كوغ	لينكس	AGPL	لا	لا	لا	المنطق الاحتمالي ، الحساب، النماذج العلائقية	سي++ ، سكيم ، بايثون	لا	تماثل الرسم البياني الفرعي
OpenSMT	لينكس ، ماك أو إس ، ويندوز	رخصة جنو العمومية الإصدار 3	جزئي الإصدار 2.0		نعم	النظرية الفارغة ، الفروق، الحساب الخطي، المتجهات الثنائية	لغة سي++	2011	محلل SMT الكسول
راسات	لينكس	رخصة جنو العمومية الإصدار 3	الإصدار 2.0			الحساب غير الخطي للأعداد الحقيقية والصحيحة		2014، 2015	توسيع نطاق انتشار قيد الفترة مع الاختبار ونظرية القيمة المتوسطة
ساتين	؟	ملكية خاصة	الإصدار 1.2			الحساب الخطي، منطق الفرق	لا أحد	2009
SMTInterpol	لينكس ، ماك أو إس ، ويندوز	LGPLv3	الإصدار 2.5			الدوال غير المفسرة، والحساب الخطي للأعداد الحقيقية، والحساب الخطي للأعداد الصحيحة	جافا	2012	يركز على توليد دوال استيفاء عالية الجودة ومضغوطة.
SMCHR	لينكس ، ماك أو إس ، ويندوز	رخصة جنو العمومية الإصدار 3	لا	لا	لا	الحساب الخطي، الحساب غير الخطي، الأكوام	ج	لا	يمكن تطبيق نظريات جديدة باستخدام قواعد معالجة القيود .
SMT-RAT	لينكس ، ماك أو إس	معهد ماساتشوستس للتكنولوجيا	الإصدار 2.0	لا	لا	الحساب الخطي، الحساب غير الخطي	لغة سي++	2015	مجموعة أدوات لحل SMT الاستراتيجي والمتوازي تتكون من مجموعة من التطبيقات المتوافقة مع SMT.
سونولار	لينكس ، ويندوز	ملكية خاصة	جزئي الإصدار 2.0			المتجهات الثنائية	ج	2010	برنامج حل SAT
حربة	لينكس ، ماك أو إس ، ويندوز	ملكية خاصة	الإصدار 1.2			المتجهات الثنائية		2008
STP	لينكس ، أوبن بي إس دي ، ويندوز ، ماك أو إس	معهد ماساتشوستس للتكنولوجيا	جزئي الإصدار 2.0	نعم	لا	المتجهات الثنائية، المصفوفات	C ، C++ ، بايثون ، OCaml ، جافا	2011	برنامج حل SAT
سيف	لينكس	ملكية خاصة	الإصدار 1.2			المتجهات الثنائية		2009
UCLID	لينكس	بي إس دي	لا	لا	لا	النظرية الفارغة ، والحساب الخطي، والمتجهات الثنائية، واللامدا المقيدة (المصفوفات، والذاكرات، وذاكرة التخزين المؤقت، وما إلى ذلك).		لا	برنامج قائم على حلّ مسائل SAT، مكتوب بلغة Moscow ML . لغة الإدخال هي مدقق نموذج SMV. موثق بشكل جيد!
فيريت	لينكس ، ماك أو إس إكس	بي إس دي	جزئي الإصدار 2.0			النظرية الفارغة ، والحساب الخطي للأعداد النسبية والصحيحة، والمكممات، والمساواة على رموز الدوال غير المفسرة.	لغة C / لغة C++	2010	يعتمد على برنامج حل SAT، ويمكنه إنتاج البراهين
ييس	لينكس ، ماك أو إس ، ويندوز ، فري بي إس دي	رخصة جنو العمومية الإصدار 3	الإصدار 2.0	لا	نعم	العمليات الحسابية الخطية للأعداد النسبية والصحيحة، والمتجهات الثنائية، والمصفوفات، والمساواة على رموز الدوال غير المفسرة.	ج	2014	شفرة المصدر متاحة عبر الإنترنت
برنامج إثبات النظريات Z3	لينكس ، ماك أو إس ، ويندوز ، فري بي إس دي	معهد ماساتشوستس للتكنولوجيا	الإصدار 2.0		نعم	نظرية الفراغ ، الحساب الخطي، الحساب غير الخطي، المتجهات الثنائية، المصفوفات، أنواع البيانات، الكميات ، السلاسل النصية	لغات البرمجة C / C++ ، و.NET ، و OCaml ، وPython ، و Java ، وHaskell	2011	شفرة المصدر متاحة عبر الإنترنت

التقييس ومسابقة حل SMT-COMP

توجد محاولات عديدة لوصف واجهة موحدة لحلّ مسائل SMT ( ومثبتات النظريات الآلية ، وهو مصطلح يُستخدم غالبًا كمرادف). أبرز هذه المحاولات معيار SMT-LIB، الذي يوفر لغةً مبنية على تعابير S. ومن بين التنسيقات الموحدة الأخرى الشائعة، تنسيق DIMACS الذي تدعمه العديد من حلّ مسائل SAT المنطقية، وتنسيق CVC الذي يستخدمه مُثبت النظريات الآلي CVC.

يأتي تنسيق SMT-LIB مزودًا بعدد من المعايير القياسية، وقد أتاح إقامة مسابقة سنوية بين برامج حل SMT تُعرف باسم SMT-COMP. في البداية، كانت المسابقة تُقام خلال مؤتمر التحقق بمساعدة الحاسوب (CAV)، ^{[ 23 ]}^{[ 24 ]} ولكن اعتبارًا من عام 2020، تُقام المسابقة كجزء من ورشة عمل SMT، التابعة للمؤتمر الدولي المشترك حول الاستدلال الآلي (IJCAR). ^{[ 25 ]}

التطبيقات

تُعدّ خوارزميات حلّ المعادلات البرمجية الرمزية (SMT) مفيدةً في كلٍّ من التحقق من صحة البرامج واختبارها بناءً على التنفيذ الرمزي ، وفي توليد أجزاء البرامج من خلال البحث في فضاء البرامج الممكنة. وإلى جانب التحقق من صحة البرامج، استُخدمت خوارزميات حلّ المعادلات البرمجية الرمزية أيضًا في استنتاج أنواع البرامج ^{[ 26 ]}^{[ 27 ]} وفي نمذجة السيناريوهات النظرية، بما في ذلك نمذجة معتقدات الجهات الفاعلة في مجال الحدّ من الأسلحة النووية ^[²⁸^] .

تَحَقّق

غالباً ما تستخدم عمليات التحقق بمساعدة الحاسوب من برامج الحاسوب خوارزميات SMT. وتتمثل إحدى التقنيات الشائعة في ترجمة الشروط المسبقة واللاحقة وشروط الحلقات والتأكيدات إلى صيغ SMT لتحديد ما إذا كانت جميع الخصائص قابلة للتحقق.

توجد العديد من أدوات التحقق المبنية على مُحلِّل Z3 SMT . تُعدّ Boogie لغة تحقق وسيطة تستخدم Z3 للتحقق التلقائي من البرامج الإجرائية البسيطة. يستخدم مُتحقق VCC للغة C المتزامنة Boogie، بالإضافة إلى Dafny للبرامج الإجرائية القائمة على الكائنات، و Chalice للبرامج المتزامنة، و Spec# للغة C#. أما F* فهي لغة ذات أنواع مُعتمدة تستخدم Z3 لإيجاد البراهين؛ حيث يُمرِّر المُصرِّف هذه البراهين لإنتاج بايت كود حامل للبرهان. تُشفِّر بنية التحقق Viper شروط التحقق إلى Z3. تُوفِّر مكتبة sbv التحقق القائم على SMT لبرامج Haskell، وتُمكِّن المستخدم من الاختيار بين عدد من المُحلِّلات مثل Z3 وABC وBoolector وcvc5 وMathSAT وYices.

توجد أيضًا العديد من أدوات التحقق المبنية على مُحلِّل Alt-Ergo SMT. إليك قائمة بالتطبيقات المُثبتة:

Why3 ، وهي منصة للتحقق من البرامج الاستنتاجية، تستخدم Alt-Ergo كأداة إثبات رئيسية لها؛
CAVEAT، وهو مدقق من الفئة C تم تطويره بواسطة CEA وتستخدمه شركة إيرباص؛ تم تضمين Alt-Ergo في تأهيل DO-178C لإحدى طائراتها الحديثة؛
يستخدم Frama-C ، وهو إطار عمل لتحليل كود C، Alt-Ergo في المكونات الإضافية Jessie و WP (المخصصة لـ "التحقق الاستنتاجي من البرنامج")؛
يستخدم SPARK CVC4 و Alt-Ergo (خلف GNATprove) لأتمتة التحقق من بعض التأكيدات في SPARK 2014؛
يمكن لـ Atelier-B استخدام Alt-Ergo بدلاً من أداة التحقق الرئيسية الخاصة به (مما يزيد من نسبة النجاح من 84٪ إلى 98٪ في معايير مشروع ANR Bware. مؤرشف في 2014-11-29 في Wayback Machine ).
يمكن لـ Rodin ، وهو إطار عمل B-method تم تطويره بواسطة Systerel، استخدام Alt-Ergo كخلفية؛
Cubicle ، وهو مدقق نماذج مفتوح المصدر للتحقق من خصائص السلامة لأنظمة الانتقال القائمة على المصفوفات.
EasyCrypt ، مجموعة أدوات للاستدلال حول الخصائص العلائقية للحسابات الاحتمالية باستخدام التعليمات البرمجية المعادية.

تُطبّق العديد من برامج حلّ المعادلات التفاضلية البسيطة (SMT) تنسيق واجهة شائعًا يُسمى SMTLIB2 (عادةً ما تكون امتدادات هذه الملفات " .smt2"). تُطبّق أداة LiquidHaskell مُدقّقًا قائمًا على نوع التحسين للغة Haskell، والذي يمكنه استخدام أي برنامج حلّ متوافق مع SMTLIB2، مثل cvc5 أو MathSat أو Z3.

التحليل والاختبار القائم على التنفيذ الرمزي

يُعدّ التنفيذ الرمزي لتحليل واختبار البرامج (مثل اختبار الترابط )، وخاصةً لاكتشاف الثغرات الأمنية، أحد أهم تطبيقات خوارزميات حل المعادلات الرمزية (SMT) . ومن الأمثلة على الأدوات في هذه الفئة: SAGE من مايكروسوفت للأبحاث ، وKLEE ، و S2E ، و Triton . أما خوارزميات حل المعادلات الرمزية المستخدمة في تطبيقات التنفيذ الرمزي فتشمل: Z3 ، وSTP ( مؤرشف بتاريخ 6 أبريل 2015 في Wayback Machine) ، وعائلة خوارزميات Z3str ، و Boolector .

إثبات النظريات التفاعلي

تم دمج حلول SMT مع مساعدي البرهان، بما في ذلك Rocq ^{[ 29 ]} و Isabelle/HOL . ^{[ 30 ]}

توليف

تُعدّ مُحلِّلات SMT لبنةً أساسيةً في توليف البرامج ، أي التوليد الآلي للبرامج من المواصفات. ومن أبرز هذه الأساليب التوليف الاستقرائي الموجه بالأمثلة المضادة (CEGIS)، حيث يقترح المُولِّد برنامجًا مرشحًا يتم التحقق منه بواسطة مُحلِّل SMT؛ وتُرشد الأمثلة المضادة الناتجة عن عمليات التحقق الفاشلة المُولِّد حتى يتم العثور على حل صحيح. ^{[ 31 ]}

ومن التطبيقات ذات الصلة إصلاح البرامج تلقائيًا : فبإعطاء برنامج به أخطاء ومجموعة اختبارات، يتم إنشاء صيغة SMT يكون حلها بمثابة تصحيح. على سبيل المثال، يقوم Nopol بترميز مشكلة إيجاد تعبير شرطي مُصلح كمثال SMT، ثم يترجم الحل مرة أخرى إلى تصحيح في شفرة المصدر لبرامج Java. ^{[ 32 ]}

انظر أيضاً

ملحوظات

↑ بلانشيت، ياسمين كريستيان؛ بومه، ساشا؛ بولسون، لورانس سي. (2013-06-01). "توسيع نطاق خوارزمية Sledgehammer باستخدام حلول SMT" . مجلة الاستدلال الآلي . 51 (1): 109-128 . doi : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . تتمتع خوارزميات ATP وحلول SMT بنقاط قوة متكاملة. تتعامل الأولى مع المحددات الكمية بكفاءة أكبر، بينما تتفوق الثانية في حل المشكلات الكبيرة، وخاصةً المشكلات الأساسية.
↑ ويبر، تجارك؛ كونشون، سيلفان؛ ديهارب، ديفيد؛ هيزمان، ماتياس؛ نيميتز، آينا؛ ريجر، جايلز (2019-01-01). " مسابقة SMT 2015-2018" . مجلة قابلية الإرضاء، والنمذجة المنطقية، والحساب . 11 (1): 221-259 . doi : 10.3233/SAT190123 . S2CID 210147712. في السنوات الأخيرة، شهدنا تداخلاً بين مسابقتي SMT-COMP وCASC، حيث تتنافس خوارزميات حل SMT في CASC، بينما تتنافس برامج ATP في SMT-COMP.
↑ باربوسا، هانيل؛ رينولدز، أندرو؛ العرواوي، دانيال؛ تينيلي، سيزار؛ باريت، كلارك (2019). "توسيع نطاق حلول SMT لتشمل منطق الرتبة العليا" . الاستدلال الآلي - CADE 27: المؤتمر الدولي السابع والعشرون للاستدلال الآلي، ناتال، البرازيل، 27-30 أغسطس 2019، وقائع المؤتمر . سبرينغر. ص 35-54 . doi : 10.1007/978-3-030-29436-6_3 . ISBN 978-3-030-29436-6. S2CID 85443815 . هال-02300986.
↑ بروتوميسو، روبرتو؛ سيماتي، أليساندرو؛ فرانزين، أندرس؛ غريجيو، ألبرتو؛ حنا، زياد؛ نادل، ألكسندر؛ بالتي، أميت؛ سيباستياني، روبرتو (2007). " حل SMT الكسول والمتعدد الطبقات لمشاكل التحقق الصناعي الصعبة" . في: دام، فيرنر؛ هيرمانز، هولجر (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 4590. برلين، هايدلبرغ: سبرينغر. الصفحات 547-560 . doi : 10.1007/978-3-540-73368-3_54 . ISBN 978-3-540-73368-3.
↑ نيوفنهاوس، ر.؛ أوليفرس، أ.؛ تينيلي، س. (2006)، "حل مسائل SAT وSAT Modulo Theories: من إجراء ديفيس-بوتنام-لوغمان-لوفلاند المجرد إلى DPLL(T)" (ملف PDF) ، مجلة ACM ، المجلد 53، الصفحات 937-977 ، doi : 10.1145/1217856.1217859 ، S2CID 14058631
↑ دي مورا، ليوناردو؛ بيورنر، نيكولاي (12-15 أغسطس 2008). "اتخاذ القرارات بفعالية باستخدام منطق القضايا باستخدام DPLL ومجموعات الاستبدال" . في: أرماندو، أليساندرو؛ باومغارتنر، بيتر؛ دويك، جيل (محررون). الاستدلال الآلي . المؤتمر الدولي المشترك الرابع حول الاستدلال الآلي، سيدني، نيو ساوث ويلز، أستراليا. سلسلة محاضرات في علوم الحاسوب. برلين، هايدلبرغ: سبرينغر. ص 410-425 . doi : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7.
↑ هادارين، ليانا؛ بانسال، كشيتيج؛ يوفانوفيتش، ديجان؛ باريت، كلارك؛ تينيلي، سيزار (2014). "قصة حلّين: نهجان متسرعان ونهجان متراخيان لمتجهات البت" . في: بيير، أرمين؛ بلوم، رودريك (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 8559. تشام: دار نشر سبرينغر الدولية. الصفحات 680-695 . doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9.
↑ براين، مارتن؛ شاندا، فلوريان؛ صن، يوتشنغ (2019). "بناء خوارزمية بت-بلاستينغ أفضل لمسائل الفاصلة العائمة". في: فوجنار، توماش؛ تشانغ، ليجون (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة . المؤتمر الدولي الخامس والعشرون، أدوات وخوارزميات لبناء وتحليل الأنظمة 2019، براغ، جمهورية التشيك، 6-11 أبريل 2019، وقائع المؤتمر، الجزء الأول. سلسلة محاضرات في علوم الحاسوب. تشام: دار نشر سبرينغر الدولية. الصفحات 79-98 . doi : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0. S2CID 92999474 .
↑ براين، مارتن؛ نيميتز، آينا؛ برينر، ماتياس؛ رينولدز، أندرو؛ باريت، كلارك؛ تينيلي، سيزار (2019). "شروط قابلية عكس صيغ الفاصلة العائمة". في: ديليغ، إيسيل؛ تاسيران، سردار (محرران). التحقق بمساعدة الحاسوب . المؤتمر الدولي الحادي والثلاثون، التحقق بمساعدة الحاسوب 2019، مدينة نيويورك، 15-18 يوليو 2019. سلسلة محاضرات في علوم الحاسوب. تشام: دار نشر سبرينغر الدولية. ص 116-136 . doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5. S2CID 196613701 .
↑ ليانغ، تياني؛ تسيسكاريدزه، نيستان؛ رينولدز، أندرو؛ تينيلي، سيزار؛ باريت، كلارك (2015). "إجراء قرار للعضوية المنتظمة وقيود الطول على السلاسل غير المحدودة" . في: لوتز، كارستن؛ رانيس، سيلفيو (محرران). آفاق أنظمة الدمج . سلسلة محاضرات في علوم الحاسوب. المجلد 9322. تشام: دار نشر سبرينغر الدولية. الصفحات 135-150 . doi : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0.
↑ رينولدز، أندرو؛ بلانشيت، ياسمين كريستيان (2015). "إجراء اتخاذ القرار لأنواع البيانات (المشتركة) في حلول SMT" . في: فيلتي، آمي ب.؛ ميدلدورب، آرت (محرران). الاستدلال الآلي - CADE-25 . سلسلة محاضرات في علوم الحاسوب. المجلد 9195. تشام: دار نشر سبرينغر الدولية. الصفحات 197-213 . doi : 10.1007/978-3-319-21401-6_13 . ISBN 978-3-319-21401-6.
↑ شينغ، يينغ؛ نوتزلي، أندريس؛ رينولدز، أندرو؛ زوهار، يوني؛ ديل، ديفيد؛ غريسكامب، وولفغانغ؛ بارك، يونكيل؛ قدير، شاز؛ باريت، كلارك؛ تينيلي، سيزار (15 سبتمبر 2023). "الاستدلال حول المتجهات: قابلية الإرضاء وفقًا لنظرية المتتاليات" . مجلة الاستدلال الآلي . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .
↑ بانسال، كشيتيج؛ رينولدز، أندرو؛ باريت، كلارك؛ تينيلي، سيزار (2016). "إجراء جديد لاتخاذ القرار للمجموعات المحدودة وقيود العدد في SMT" . في: أوليفيتي، نيكولا؛ تيواري، أشيش (محرران). الاستدلال الآلي . سلسلة محاضرات في علوم الحاسوب. المجلد 9706. تشام: دار نشر سبرينغر الدولية. الصفحات 82-98 . doi : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1.
↑ مينغ، باولو؛ رينولدز، أندرو؛ تينيلي، سيزار؛ باريت، كلارك (2017). "حل القيود العلائقية في SMT" . في دي مورا، ليوناردو (محرر). الاستدلال الآلي - CADE 26. سلسلة محاضرات في علوم الحاسوب. المجلد 10395. تشام: دار نشر سبرينغر الدولية. الصفحات 148-165 . doi : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5.
↑ رينولدز، أندرو؛ يوسف، رادو؛ سربان، كريستينا؛ كينغ، تيم (2016). "إجراء اتخاذ القرار لمنطق الفصل في SMT" . في: آرثو، سيريل؛ ليجاي، أكسل؛ بيليد، دورون (محررون). التكنولوجيا الآلية للتحقق والتحليل . سلسلة محاضرات في علوم الحاسوب. المجلد 9938. تشام: دار نشر سبرينغر الدولية. الصفحات 244-261 . doi : 10.1007/978-3-319-46520-3_16 . ISBN 978-3-319-46520-3. S2CID 6753369 .
↑ أوزدمير، أليكس؛ كريمر، جيريون؛ تينيلي، سيزار؛ باريت، كلارك (2023). "قابلية الإرضاء بتردد الحقول المنتهية" . في: إينيا، قسطنطين؛ لال، أكاش (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 13965. تشام: سبرينغر نيتشر سويسرا. الصفحات 163-186 . doi : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7. S2CID 257235627 .
↑ بايلس، سام؛ بايلس، نوح؛ هوس، هولجر؛ هو، آلان (4 مارس 2015). "SAT Modulo Monotonic Theories" . وقائع مؤتمر AAAI حول الذكاء الاصطناعي . 29 (1). arXiv : 1406.0043 . doi : 10.1609/aaai.v29i1.9755 . ISSN 2374-3468 . S2CID 9567647 .
^ كلينزي، توبياس؛ بايليس، سام؛ هو، آلان ج. (2016). "توليف CTL سريع ومرن وبسيط عبر SMT" . في تشودوري، سوارات؛ فرزان، أزاده (محرران). التحقق بمساعدة الكمبيوتر . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 9779. شام: سبرينغر الدولية للنشر. ص 136 – 156. دوى : 10.1007 / 978-3-319-41528-4_8 . رقم ISBN 978-3-319-41528-4.
↑ بيمبينك، آرون؛ غرينبيرغ، مايكل؛ تشونغ، ستيفن (11 يناير 2023). "من SMT إلى ASP: مناهج قائمة على المُحلِّل لحل مشاكل توليف Datalog كاختيار قاعدة" . وقائع مؤتمر ACM حول لغات البرمجة . 7 (POPL): 7:185–7:217. doi : 10.1145/3571200 . S2CID 253525805 .
↑ باور، أ.؛ بيستر، م.؛ تاوتشنيغ، م. (2007)، "دعم الأدوات لتحليل الأنظمة والنماذج الهجينة"، وقائع مؤتمر 2007 حول التصميم والأتمتة والاختبار في أوروبا (DATE'07) ، جمعية مهندسي الكهرباء والإلكترونيات، ص 1، CiteSeerX 10.1.1.323.6807 ، doi : 10.1109/DATE.2007.364411 ، ISBN 978-3-9810801-2-4، S2CID 9159847
↑ فرانزل، م.؛ هيردي، س.؛ راتشان، س.؛ شوبرت، ت.؛ تايج، ت. (2007)، "حل فعال لأنظمة القيود الحسابية غير الخطية الكبيرة ذات البنية البوليانية المعقدة" (ملف PDF) ، مجلة قابلية الإرضاء، والنمذجة البوليانية، والحساب ، 1 (3-4 عدد خاص من JSAT حول تكامل SAT/CP): 209-236 ، doi : 10.3233/SAT190012
↑ باربوسا، هانيل؛ باريت، كلارك؛ براين، مارتن؛ كريمر، جيريون؛ لاخنيت، حنا؛ مان، ماكاي؛ محمد، عبد الرحمن؛ محمد، مدثر؛ نيميتز، آينا؛ نوتزلي، أندريس؛ أوزدمير، أليكس؛ برينر، ماتياس؛ رينولدز، أندرو؛ شينغ، يينغ؛ تينيلي، سيزار (2022). "cvc5: برنامج حل SMT متعدد الاستخدامات وقوي على مستوى الصناعة" . في: فيسمان، دانا؛ روسو، غريغوري (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة، المؤتمر الدولي الثامن والعشرون . سلسلة محاضرات في علوم الحاسوب. المجلد 13243. تشام: دار نشر سبرينغر الدولية. ص 415 – 442. دوى : 10.1007 / 978-3-030-99524-9_24 . رقم ISBN 978-3-030-99524-9. S2CID 247857361 .
↑ باريت، كلارك؛ دي مورا، ليوناردو؛ ستامب، آرون (2005). "SMT-COMP: منافسة قابلية الإرضاء وفقًا للنظريات" . في: إتيسامي، كوشا؛ راجاماني، سريرام ك. (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 3576. سبرينغر. الصفحات 20-23 . doi : 10.1007/11513988_4 . ISBN 978-3-540-31686-2.
↑ باريت، كلارك؛ دي مورا، ليوناردو؛ رانيس، سيلفيو؛ ستامب، آرون؛ تينيلي، سيزار (2011). "مبادرة SMT-LIB وصعود SMT: (محاضرة جائزة HVC 2010)". في: بارنر، شارون؛ هاريس، إيان؛ كرونينج، دانيال؛ راز، أورنا (محررون). الأجهزة والبرمجيات: التحقق والاختبار . سلسلة محاضرات في علوم الحاسوب. المجلد 6504. سبرينغر. ص 3. Bibcode : 2011LNCS.6504....3B . doi : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.
↑ "SMT-COMP 2020" . SMT-COMP . تم الاطلاع عليه بتاريخ 19-10-2020 .
↑ حسن، مصطفى؛ أوربان، كاترينا؛ إيلرز، ماركو؛ مولر، بيتر (2018). "استدلال النوع القائم على MaxSMT للغة بايثون 3" . التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10982. الصفحات 12-19 . doi : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5.
↑ لونكاريك، كالفن، وآخرون. "إطار عمل عملي لتفسير خطأ استنتاج النوع." ACM SIGPLAN Notices 51.10 (2016): 781-799.
↑ بومونت، بول؛ إيفانز، نيل؛ هوث، مايكل؛ بلانت، توم (2015). "تحليل الثقة للحد من التسلح النووي: تجريدات SMT لشبكات الاعتقاد البايزية". في بيرنول، غونتر؛ يا رايان، بيتر؛ ويبل، إدغار (محررون). أمن الحاسوب - ESORICS 2015. سلسلة محاضرات في علوم الحاسوب. المجلد 9326. سبرينغر. الصفحات 521-540 . doi : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.
↑ إيكيتشي، بوراك؛ ميبسوت، آلان؛ تينيلي، سيزار؛ كيلر، شانتال؛ كاتز، غاي؛ رينولدز، أندرو؛ باريت، كلارك (2017). "SMTCoq: إضافة لدمج حلول SMT في Coq" . في: ماجومدار، روباك؛ كونكاك، فيكتور (محرران). التحقق بمساعدة الحاسوب، المؤتمر الدولي التاسع والعشرون . سلسلة محاضرات في علوم الحاسوب. المجلد 10427. تشام: دار نشر سبرينغر الدولية. الصفحات 126-133 . doi : 10.1007/978-3-319-63390-9_7 . ISBN 978-3-319-63390-9. S2CID 206701576 .
↑ بلانشيت، ياسمين كريستيان؛ بومه، ساشا؛ بولسون، لورانس سي. (2013-06-01). "توسيع نطاق خوارزمية Sledgehammer باستخدام حلول SMT" . مجلة الاستدلال الآلي . 51 (1): 109-128 . doi : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 .
↑ أباتي، أليساندرو؛ ديفيد، كريستينا؛ كيسيلي، باسكال؛ كرونينغ، دانيال؛ بولغرين، إليزابيث (2018). "التوليف الاستقرائي الموجه بالأمثلة المضادة وفقًا للنظريات". التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10981. الصفحات 270-288 . doi : 10.1007/978-3-319-96145-3_15 . ISBN 978-3-319-96144-6.
↑ شوان، جيفنغ؛ مارتينيز، ماتياس؛ ديماركو، فافيو؛ كليمنت، ماكسيم؛ ماركوت، سيباستيان لاملاس؛ دوريو، توماس؛ لو بير، دانيال؛ مونبيروس، مارتن (يناير 2017). "نوبول: الإصلاح التلقائي لأخطاء العبارات الشرطية في برامج جافا". معاملات IEEE في هندسة البرمجيات . 43 (1): 34-55 . arXiv : 1811.04211 . Bibcode : 2017ITSEn..43...34X . doi : 10.1109/tse.2016.2560811 .

مراجع

باريت، سي.؛ سيباستياني، ر.؛ سيشيا، س.؛ تينيلي، سي. (2009). "قابلية الإرضاء وفقًا للنظريات" . في: بيير، أ.؛ هيول، إم جيه إتش؛ فان مارين، إتش.؛ والش، تي. (محررون). دليل قابلية الإرضاء . آفاق في الذكاء الاصطناعي وتطبيقاته. المجلد 185. دار نشر IOS. الصفحات 825-885 . ISBN 9781607503767.
غانيش، فيجاي (سبتمبر 2007). إجراءات اتخاذ القرار للمتجهات الثنائية والمصفوفات والأعداد الصحيحة (ملف PDF) (أطروحة دكتوراه). قسم علوم الحاسوب، جامعة ستانفورد.
جها، سوسميت؛ ليماي، ريشيكيش؛ سيشيا، سانجيت أ. (2009). "بيفر: هندسة حلّ SMT فعّال لحسابات المتجهات الثنائية". وقائع المؤتمر الدولي الحادي والعشرين حول التحقق بمساعدة الحاسوب . الصفحات 668-674 . doi : 10.1007/978-3-642-02658-4_53 . ISBN 978-3-642-02658-4.
براينت، ر. إي.؛ جيرمان، س. م.؛ فيليف، م. ن. (1999). "التحقق من المعالجات الدقيقة باستخدام إجراءات اتخاذ القرار الفعالة لمنطق المساواة مع الدوال غير المفسرة" (ملف PDF) . الجداول التحليلية والأساليب ذات الصلة . الصفحات 1-13 . ، ص. ، .
ديفيس، م.؛ بوتنام، هـ. (1960). "إجراء حسابي لنظرية التكميم" . مجلة رابطة آلات الحوسبة . 7 (3): 201-215 . doi : 10.1145/321033.321034 . S2CID 31888376 .
ديفيس، م.؛ لوغيمان، ج.؛ لوفلاند، د. (1962). "برنامج آلي لإثبات النظريات". اتصالات رابطة آلات الحوسبة . 5 (7): 394-397 . doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
كرونينغ، د.؛ ستريشمان، أ. (2008). إجراءات اتخاذ القرار - منظور خوارزمي . سلسلة علوم الحاسوب النظرية. سبرينغر. ISBN 978-3-540-74104-6.
نام، جي.-جيه.؛ ساكالا، كيه. إيه.؛ روتنبار، آر. (2002). "نهج جديد للتوجيه التفصيلي في الدوائر المتكاملة القابلة للبرمجة (FPGA) عبر إمكانية الإرضاء المنطقي القائم على البحث". معاملات IEEE في التصميم بمساعدة الحاسوب للدوائر والأنظمة المتكاملة . 21 (6): 674-684 . رمز Bibcode : 2002ITCAD..21..674N . doi : 10.1109/TCAD.2002.1004311 .
مكتبة SMT-LIB: مكتبة قابلية الإرضاء المعياري للنظريات
مسابقة SMT-COMP: مسابقة قابلية الإرضاء المعيارية للنظريات
إجراءات اتخاذ القرار - من منظور خوارزمي
سيباستياني، ر. (2007). "قابلية الإرضاء الكسولة وفقًا للنظريات". مجلة قابلية الإرضاء، والنمذجة المنطقية، والحساب . 3 ( 3-4 ): 141-224 . CiteSeerX 10.1.1.100.221 . doi : 10.3233/SAT190034 .

هذه المقالة مقتبسة في الأصل من عمود في النشرة الإلكترونية لجمعية ACM SIGDA بقلم كارم أ. ساكالا . النص الأصلي متاح هنا .

[1] بلانشيت، ياسمين كريستيان؛ بومه، ساشا؛ بولسون، لورانس سي. (2013-06-01). "توسيع نطاق خوارزمية Sledgehammer باستخدام حلول SMT" . مجلة الاستدلال الآلي . 51 (1): 109-128 . doi : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . تتمتع خوارزميات ATP وحلول SMT بنقاط قوة متكاملة. تتعامل الأولى مع المحددات الكمية بكفاءة أكبر، بينما تتفوق الثانية في حل المشكلات الكبيرة، وخاصةً المشكلات الأساسية.

[2] ويبر، تجارك؛ كونشون، سيلفان؛ ديهارب، ديفيد؛ هيزمان، ماتياس؛ نيميتز، آينا؛ ريجر، جايلز (2019-01-01). " مسابقة SMT 2015-2018" . مجلة قابلية الإرضاء، والنمذجة المنطقية، والحساب . 11 (1): 221-259 . doi : 10.3233/SAT190123 . S2CID 210147712. في السنوات الأخيرة، شهدنا تداخلاً بين مسابقتي SMT-COMP وCASC، حيث تتنافس خوارزميات حل SMT في CASC، بينما تتنافس برامج ATP في SMT-COMP.

[3] باربوسا، هانيل؛ رينولدز، أندرو؛ العرواوي، دانيال؛ تينيلي، سيزار؛ باريت، كلارك (2019). "توسيع نطاق حلول SMT لتشمل منطق الرتبة العليا" . الاستدلال الآلي - CADE 27: المؤتمر الدولي السابع والعشرون للاستدلال الآلي، ناتال، البرازيل، 27-30 أغسطس 2019، وقائع المؤتمر . سبرينغر. ص 35-54 . doi : 10.1007/978-3-030-29436-6_3 . ISBN 978-3-030-29436-6. S2CID 85443815 . هال-02300986.

[4] بروتوميسو، روبرتو؛ سيماتي، أليساندرو؛ فرانزين، أندرس؛ غريجيو، ألبرتو؛ حنا، زياد؛ نادل، ألكسندر؛ بالتي، أميت؛ سيباستياني، روبرتو (2007). " حل SMT الكسول والمتعدد الطبقات لمشاكل التحقق الصناعي الصعبة" . في: دام، فيرنر؛ هيرمانز، هولجر (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 4590. برلين، هايدلبرغ: سبرينغر. الصفحات 547-560 . doi : 10.1007/978-3-540-73368-3_54 . ISBN 978-3-540-73368-3.

[5] نيوفنهاوس، ر.؛ أوليفرس، أ.؛ تينيلي، س. (2006)، "حل مسائل SAT وSAT Modulo Theories: من إجراء ديفيس-بوتنام-لوغمان-لوفلاند المجرد إلى DPLL(T)" (ملف PDF) ، مجلة ACM ، المجلد 53، الصفحات 937-977 ، doi : 10.1145/1217856.1217859 ، S2CID 14058631

[6] دي مورا، ليوناردو؛ بيورنر، نيكولاي (12-15 أغسطس 2008). "اتخاذ القرارات بفعالية باستخدام منطق القضايا باستخدام DPLL ومجموعات الاستبدال" . في: أرماندو، أليساندرو؛ باومغارتنر، بيتر؛ دويك، جيل (محررون). الاستدلال الآلي . المؤتمر الدولي المشترك الرابع حول الاستدلال الآلي، سيدني، نيو ساوث ويلز، أستراليا. سلسلة محاضرات في علوم الحاسوب. برلين، هايدلبرغ: سبرينغر. ص 410-425 . doi : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7.

[7] هادارين، ليانا؛ بانسال، كشيتيج؛ يوفانوفيتش، ديجان؛ باريت، كلارك؛ تينيلي، سيزار (2014). "قصة حلّين: نهجان متسرعان ونهجان متراخيان لمتجهات البت" . في: بيير، أرمين؛ بلوم، رودريك (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 8559. تشام: دار نشر سبرينغر الدولية. الصفحات 680-695 . doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9.

[8] براين، مارتن؛ شاندا، فلوريان؛ صن، يوتشنغ (2019). "بناء خوارزمية بت-بلاستينغ أفضل لمسائل الفاصلة العائمة". في: فوجنار، توماش؛ تشانغ، ليجون (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة . المؤتمر الدولي الخامس والعشرون، أدوات وخوارزميات لبناء وتحليل الأنظمة 2019، براغ، جمهورية التشيك، 6-11 أبريل 2019، وقائع المؤتمر، الجزء الأول. سلسلة محاضرات في علوم الحاسوب. تشام: دار نشر سبرينغر الدولية. الصفحات 79-98 . doi : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0. S2CID 92999474 .

[9] براين، مارتن؛ نيميتز، آينا؛ برينر، ماتياس؛ رينولدز، أندرو؛ باريت، كلارك؛ تينيلي، سيزار (2019). "شروط قابلية عكس صيغ الفاصلة العائمة". في: ديليغ، إيسيل؛ تاسيران، سردار (محرران). التحقق بمساعدة الحاسوب . المؤتمر الدولي الحادي والثلاثون، التحقق بمساعدة الحاسوب 2019، مدينة نيويورك، 15-18 يوليو 2019. سلسلة محاضرات في علوم الحاسوب. تشام: دار نشر سبرينغر الدولية. ص 116-136 . doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5. S2CID 196613701 .

[10] ليانغ، تياني؛ تسيسكاريدزه، نيستان؛ رينولدز، أندرو؛ تينيلي، سيزار؛ باريت، كلارك (2015). "إجراء قرار للعضوية المنتظمة وقيود الطول على السلاسل غير المحدودة" . في: لوتز، كارستن؛ رانيس، سيلفيو (محرران). آفاق أنظمة الدمج . سلسلة محاضرات في علوم الحاسوب. المجلد 9322. تشام: دار نشر سبرينغر الدولية. الصفحات 135-150 . doi : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0.

[11] رينولدز، أندرو؛ بلانشيت، ياسمين كريستيان (2015). "إجراء اتخاذ القرار لأنواع البيانات (المشتركة) في حلول SMT" . في: فيلتي، آمي ب.؛ ميدلدورب، آرت (محرران). الاستدلال الآلي - CADE-25 . سلسلة محاضرات في علوم الحاسوب. المجلد 9195. تشام: دار نشر سبرينغر الدولية. الصفحات 197-213 . doi : 10.1007/978-3-319-21401-6_13 . ISBN 978-3-319-21401-6.

[12] شينغ، يينغ؛ نوتزلي، أندريس؛ رينولدز، أندرو؛ زوهار، يوني؛ ديل، ديفيد؛ غريسكامب، وولفغانغ؛ بارك، يونكيل؛ قدير، شاز؛ باريت، كلارك؛ تينيلي، سيزار (15 سبتمبر 2023). "الاستدلال حول المتجهات: قابلية الإرضاء وفقًا لنظرية المتتاليات" . مجلة الاستدلال الآلي . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .

[13] بانسال، كشيتيج؛ رينولدز، أندرو؛ باريت، كلارك؛ تينيلي، سيزار (2016). "إجراء جديد لاتخاذ القرار للمجموعات المحدودة وقيود العدد في SMT" . في: أوليفيتي، نيكولا؛ تيواري، أشيش (محرران). الاستدلال الآلي . سلسلة محاضرات في علوم الحاسوب. المجلد 9706. تشام: دار نشر سبرينغر الدولية. الصفحات 82-98 . doi : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1.

[14] مينغ، باولو؛ رينولدز، أندرو؛ تينيلي، سيزار؛ باريت، كلارك (2017). "حل القيود العلائقية في SMT" . في دي مورا، ليوناردو (محرر). الاستدلال الآلي - CADE 26. سلسلة محاضرات في علوم الحاسوب. المجلد 10395. تشام: دار نشر سبرينغر الدولية. الصفحات 148-165 . doi : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5.

[15] رينولدز، أندرو؛ يوسف، رادو؛ سربان، كريستينا؛ كينغ، تيم (2016). "إجراء اتخاذ القرار لمنطق الفصل في SMT" . في: آرثو، سيريل؛ ليجاي، أكسل؛ بيليد، دورون (محررون). التكنولوجيا الآلية للتحقق والتحليل . سلسلة محاضرات في علوم الحاسوب. المجلد 9938. تشام: دار نشر سبرينغر الدولية. الصفحات 244-261 . doi : 10.1007/978-3-319-46520-3_16 . ISBN 978-3-319-46520-3. S2CID 6753369 .

[16] أوزدمير، أليكس؛ كريمر، جيريون؛ تينيلي، سيزار؛ باريت، كلارك (2023). "قابلية الإرضاء بتردد الحقول المنتهية" . في: إينيا، قسطنطين؛ لال، أكاش (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 13965. تشام: سبرينغر نيتشر سويسرا. الصفحات 163-186 . doi : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7. S2CID 257235627 .

[17] بايلس، سام؛ بايلس، نوح؛ هوس، هولجر؛ هو، آلان (4 مارس 2015). "SAT Modulo Monotonic Theories" . وقائع مؤتمر AAAI حول الذكاء الاصطناعي . 29 (1). arXiv : 1406.0043 . doi : 10.1609/aaai.v29i1.9755 . ISSN 2374-3468 . S2CID 9567647 .

[18] كلينزي، توبياس؛ بايليس، سام؛ هو، آلان ج. (2016). "توليف CTL سريع ومرن وبسيط عبر SMT" . في تشودوري، سوارات؛ فرزان، أزاده (محرران). التحقق بمساعدة الكمبيوتر . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 9779. شام: سبرينغر الدولية للنشر. ص 136 – 156. دوى : 10.1007 / 978-3-319-41528-4_8 . رقم ISBN 978-3-319-41528-4.

[19] بيمبينك، آرون؛ غرينبيرغ، مايكل؛ تشونغ، ستيفن (11 يناير 2023). "من SMT إلى ASP: مناهج قائمة على المُحلِّل لحل مشاكل توليف Datalog كاختيار قاعدة" . وقائع مؤتمر ACM حول لغات البرمجة . 7 (POPL): 7:185–7:217. doi : 10.1145/3571200 . S2CID 253525805 .

[20] باور، أ.؛ بيستر، م.؛ تاوتشنيغ، م. (2007)، "دعم الأدوات لتحليل الأنظمة والنماذج الهجينة"، وقائع مؤتمر 2007 حول التصميم والأتمتة والاختبار في أوروبا (DATE'07) ، جمعية مهندسي الكهرباء والإلكترونيات، ص 1، CiteSeerX 10.1.1.323.6807 ، doi : 10.1109/DATE.2007.364411 ، ISBN 978-3-9810801-2-4، S2CID 9159847

[21] فرانزل، م.؛ هيردي، س.؛ راتشان، س.؛ شوبرت، ت.؛ تايج، ت. (2007)، "حل فعال لأنظمة القيود الحسابية غير الخطية الكبيرة ذات البنية البوليانية المعقدة" (ملف PDF) ، مجلة قابلية الإرضاء، والنمذجة البوليانية، والحساب ، 1 (3-4 عدد خاص من JSAT حول تكامل SAT/CP): 209-236 ، doi : 10.3233/SAT190012

[22] باربوسا، هانيل؛ باريت، كلارك؛ براين، مارتن؛ كريمر، جيريون؛ لاخنيت، حنا؛ مان، ماكاي؛ محمد، عبد الرحمن؛ محمد، مدثر؛ نيميتز، آينا؛ نوتزلي، أندريس؛ أوزدمير، أليكس؛ برينر، ماتياس؛ رينولدز، أندرو؛ شينغ، يينغ؛ تينيلي، سيزار (2022). "cvc5: برنامج حل SMT متعدد الاستخدامات وقوي على مستوى الصناعة" . في: فيسمان، دانا؛ روسو، غريغوري (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة، المؤتمر الدولي الثامن والعشرون . سلسلة محاضرات في علوم الحاسوب. المجلد 13243. تشام: دار نشر سبرينغر الدولية. ص 415 – 442. دوى : 10.1007 / 978-3-030-99524-9_24 . رقم ISBN 978-3-030-99524-9. S2CID 247857361 .

[23] باريت، كلارك؛ دي مورا، ليوناردو؛ ستامب، آرون (2005). "SMT-COMP: منافسة قابلية الإرضاء وفقًا للنظريات" . في: إتيسامي، كوشا؛ راجاماني، سريرام ك. (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 3576. سبرينغر. الصفحات 20-23 . doi : 10.1007/11513988_4 . ISBN 978-3-540-31686-2.

[24] باريت، كلارك؛ دي مورا، ليوناردو؛ رانيس، سيلفيو؛ ستامب، آرون؛ تينيلي، سيزار (2011). "مبادرة SMT-LIB وصعود SMT: (محاضرة جائزة HVC 2010)". في: بارنر، شارون؛ هاريس، إيان؛ كرونينج، دانيال؛ راز، أورنا (محررون). الأجهزة والبرمجيات: التحقق والاختبار . سلسلة محاضرات في علوم الحاسوب. المجلد 6504. سبرينغر. ص 3. Bibcode : 2011LNCS.6504....3B . doi : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.

[25] "SMT-COMP 2020" . SMT-COMP . تم الاطلاع عليه بتاريخ 19-10-2020 .

[26] حسن، مصطفى؛ أوربان، كاترينا؛ إيلرز، ماركو؛ مولر، بيتر (2018). "استدلال النوع القائم على MaxSMT للغة بايثون 3" . التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10982. الصفحات 12-19 . doi : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5.

[27] لونكاريك، كالفن، وآخرون. "إطار عمل عملي لتفسير خطأ استنتاج النوع." ACM SIGPLAN Notices 51.10 (2016): 781-799.

[28] بومونت، بول؛ إيفانز، نيل؛ هوث، مايكل؛ بلانت، توم (2015). "تحليل الثقة للحد من التسلح النووي: تجريدات SMT لشبكات الاعتقاد البايزية". في بيرنول، غونتر؛ يا رايان، بيتر؛ ويبل، إدغار (محررون). أمن الحاسوب - ESORICS 2015. سلسلة محاضرات في علوم الحاسوب. المجلد 9326. سبرينغر. الصفحات 521-540 . doi : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.

[29] إيكيتشي، بوراك؛ ميبسوت، آلان؛ تينيلي، سيزار؛ كيلر، شانتال؛ كاتز، غاي؛ رينولدز، أندرو؛ باريت، كلارك (2017). "SMTCoq: إضافة لدمج حلول SMT في Coq" . في: ماجومدار، روباك؛ كونكاك، فيكتور (محرران). التحقق بمساعدة الحاسوب، المؤتمر الدولي التاسع والعشرون . سلسلة محاضرات في علوم الحاسوب. المجلد 10427. تشام: دار نشر سبرينغر الدولية. الصفحات 126-133 . doi : 10.1007/978-3-319-63390-9_7 . ISBN 978-3-319-63390-9. S2CID 206701576 .

[30] بلانشيت، ياسمين كريستيان؛ بومه، ساشا؛ بولسون، لورانس سي. (2013-06-01). "توسيع نطاق خوارزمية Sledgehammer باستخدام حلول SMT" . مجلة الاستدلال الآلي . 51 (1): 109-128 . doi : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 .

[31] أباتي، أليساندرو؛ ديفيد، كريستينا؛ كيسيلي، باسكال؛ كرونينغ، دانيال؛ بولغرين، إليزابيث (2018). "التوليف الاستقرائي الموجه بالأمثلة المضادة وفقًا للنظريات". التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10981. الصفحات 270-288 . doi : 10.1007/978-3-319-96145-3_15 . ISBN 978-3-319-96144-6.

[32] شوان، جيفنغ؛ مارتينيز، ماتياس؛ ديماركو، فافيو؛ كليمنت، ماكسيم؛ ماركوت، سيباستيان لاملاس؛ دوريو، توماس؛ لو بير، دانيال؛ مونبيروس، مارتن (يناير 2017). "نوبول: الإصلاح التلقائي لأخطاء العبارات الشرطية في برامج جافا". معاملات IEEE في هندسة البرمجيات . 43 (1): 34-55 . arXiv : 1811.04211 . Bibcode : 2017ITSEn..43...34X . doi : 10.1109/tse.2016.2560811 .

[ 1 ]

[ 2 ]

[

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[

[

[

[

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25 ]

[ 26 ]

[ 27 ]

[

[ 29 ]

[ 30 ]

[ 31 ]

[ 32 ]

اللغة	العربية (RTL)
روابط موسوعية	30 رابطاً
المصدر الأصلي	ويكيبيديا ↗