حساب عدد النماذج الراضية - مع مراعاة القيود الرياضية

Question

سؤال

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

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

مثال

نحن نمثل الصيغة المنطقية $Q = (أ \أو ب) \إسفين (ج \أو د)$ مثل القيود $$a + b \geq 1 \\ c + d \geq 1$$ أو كمصفوفة $أ$ وناقل الدعم $ب$ ستر

حيث كافة المتغيرات $a,b,c,d \في \{0,1\}$.نحن نعلم أن هناك برامج تأخذ $س$ كمدخل ومخرج عدد التفسيرات ولكن هل هناك برامج مأخوذة $أ$ و $ب$ كمدخل (أو بناء مماثل) ومخرجات نفس العدد من التفسيرات؟

Answer 1

أعرف طريقتين معقولتين.

النهج رقم 1: احسب عدد النقاط الصحيحة داخل متعدد الأضلاع المحدب.

مجموعة المتباينات الخطية التي قدمتها، بالإضافة إلى المتباينات $0 \le a,b,c,d \le 1$, ، يحدد polytope محدب.الآن، تريد أن حساب عدد النقاط الصحيحة التي تقع ضمن هذا polytope.

هناك خوارزميات قياسية للقيام بذلك، والتي يمكنك تطبيقها مباشرة.إذا بحثت عن "عد النقاط الصحيحة في polytope" أو "عد نقاط الشبكة في polytope" فستجد العديد من الأوراق البحثية.انظر، على سبيل المثال، https://cstheory.stackexchange.com/q/22280/5038, إيجاد جميع الحلول لمشكلة البرمجة الخطية للأعداد الصحيحة (ILP)..

النهج رقم 2: قم بالتحويل إلى CNF، ثم استخدم برنامج #SAT.

يمكنك دائمًا تحويل القيود الخاصة بك إلى صيغة CNF.يمكن تحويل كل متباينة خطية إلى مجموعة من عبارات CNF.عدم المساواة الخطية للنموذج $x_i + \dots + x_j \ge 1$ يتوافق على الفور مع جملة CNF $(x_i \lor \dots \lor x_j)$.للحصول على عدم مساواة خطية أكثر عمومية للنموذج $x_i + \dots + x_j \ge c$, ، تريد التعبير عن القيد على الأقل $ج$ خارج ال $ك$ المتغيرات $x_i,\dots,x_j$ صحيحة.هناك العديد من الطرق القياسية لتشفير ذلك.يرى https://cstheory.stackexchange.com/q/23771/5038, قم بتقليل المشكلة التالية إلى SAT, ترميز القيد 1-out-of-n لمحللي SAT,

(أحد الأساليب هو تحويل دائرة منطقية تحسب $x_i + \dots + x_j$ ويقارن بها $ج$, ، ثم قم بتحويل الدائرة المنطقية إلى CNF باستخدام تحويل تسيتين.يمكنك إنشاء مثل هذه الدائرة المنطقية باستخدام دوائر المقارنة والمقارنة القياسية.ومع ذلك، هناك العديد من الطرق الأخرى أيضًا.)

بمجرد حصولك على صيغة CNF تعادل مجموعة القيود، يمكنك استخدام أي حل #SAT جاهز لحساب عدد الحلول لصيغة CNF تلك.

---

من الصعب أن نقول أي من هذين النهجين سوف يعمل بشكل أفضل؛قد تحتاج إلى تجربتهما على أنواع الحالات التي تتعامل معها، لتعرف ذلك على وجه اليقين.أتوقع ذلك إذا كان لديك عدم مساواة خطية في النموذج $x_i + \dots + x_j \ge c$ أين $ج$ إذا كان كبيرًا، فقد يكون النهج رقم 1 متفوقًا؛لكن اذا $ج$ إذا كان صغيرًا عادةً، فقد يكون النهج رقم 2 متفوقًا.

Answer 2

يمكنك تنفيذ DPLL باستخدام القيود مباشرة بدلاً من الجمل.وهذا يتطلب تعديل بنية البيانات وخوارزمية الانتشار، ولكنها تعمل بنفس الطريقة.

بمجرد تعيين كافة متغيرات القيد باستثناء متغير واحد، قد يحدث انتشار الوحدة.

بمجرد تعيين كافة متغيرات القيد، قد يحدث تعارض.

تبقى بقية الخوارزمية كما هي.

القيد على المتغيرات المنطقية هو مجرد مجموعة من عبارات CNF المخفية (من المحتمل أن يكون هناك العديد من العبارات بشكل كبير اعتمادًا على القيد).

Answer 3

لقد كان السؤال أجاب على or.stackexchange لبرامج البرمجة ذات الأعداد الصحيحة المختلطة، مع أمثلة على البرامج والبرامج النصية الموجودة (CPLEX، SCIP، ...).

هذا يشبه خوارزمية CDCL أكثر من DPLL:وعندما يتم العثور على حل جديد، يضاف قيد جديد لمنعه ويستأنف البحث، حتى تصبح المشكلة غير ممكنة.