هل من الممكن حل مشكلة غطاء المجموعة الفرعية هذه باستخدام محلل SAT؟

Question

المشكلة هي أن تجد $\mathcal{S}$, ، الحد الأدنى من جمع مجموعات فرعية من $\{1،\النقاط، 17\}$ بحيث يتوفر الشرطان:

1. لو $S \subseteq \mathcal{S}$ ثم $|S|=6$;
2. لأي $A \subseteq \{1,\dots,17\}$ مع $|أ|=3$, ، يوجد أ $S \في \mathcal{S}$ مع $A \مجموعة فرعية S$.

يرى هنا لمشكلة اندماجية ذات صلة.

أعتقد أن هذا يمكن صياغته كمشكلة Min SAT.

لكل $S \subseteq \{1,\dots,17\}$ مع $|S|=6$, ، نقدم متغيرًا $X_S$.ولكل $A \subseteq \{1,\dots,17\}$ مع $|أ|=3$, ، نقدم جملة$$ vee_ {s:a subseteq s ، | s | = 6} x_ {s} $$ثم يمكننا من حيث المبدأ استخدام برنامج SAT للعثور على أقل عدد ممكن من الملفات $X_S$ يجب أن يكون صحيحًا لتلبية جميع الشروط.

هذا يحتاج $\binom{17}{6}=12376$ المتغيرات، $\binom{17}{3}=680$ أحكام الطول $\binom{17-3}{3}=364$.

لدي خبرة قليلة جدًا في استخدام حلول SAT فعليًا.فهل هذا بالفعل يستحق المحاولة على جهاز الكمبيوتر المحمول الخاص بي أم أنه لا يوجد أمل على الإطلاق؟

——-

تحديث

تبين أن هناك العديد من الأبحاث حول مجموعة التغطية.يبدو أنني كنت طموحاً أكثر من اللازم لمحاولة حل مشكلة المعلمات (17، 6، 3).

إنها بالفعل مشكلة مفتوحة لـ (12، 5، 3).

يرى هنا لمزيد من التفاصيل.

———

تحديث 2

حاولت كتابة كل شيء بلغة SAT الخالصة وكان الأمر قليلًا جدًا أسرع باستخدام cadical من z3.

كما أن العثور على حل أسرع بكثير من إظهار عدم وجود حلول.

لقد حاولت كسر التماثل عن طريق إضافة القيود التي تتطلب تحديد المجموعة الفرعية الأولى والأخيرة في ترتيب المعجم.

Answer 1

يُشار عادةً إلى التحسين باستخدام SAT باسم MaxSAT بدلاً من Min SAT.على وجه الخصوص، أقترح البحث عن حلول لـ "MaxSAT الجزئي الموزون"، على سبيل المثال MaxHS وRC2.

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

Answer 2

مع اختبار SAT، قد يكون من الصعب التنبؤ بما سيكون ممكنًا وما لن يكون ممكنًا.الأمر يستحق المحاولة.

أود أن أقترح عليك أولاً، بدلاً من MinSAT، أن تحاول استخدام البحث الثنائي $n=|\mathcal{S}|$, ، عدد المجموعات التي تحتاجها.يمكنك استخدام على الأكثر-$ن$-خارج القيد 12376 على الخاص بك $X_S$ المتغيرات.هناك عديد التقنيات ل ترميز ذلك في SAT، على الرغم من أنني سأحاول استخدامه أولاً في الممارسة العملية PbLe مع حلالا Z3.

مشكلتك لديها الكثير من التماثل.قد تواجه حلول SAT أحيانًا صعوبة في التناظر.قد تحاول أن تفعل قدر ما تستطيع لكسر التماثل.على سبيل المثال، دون فقدان العمومية يمكننا أن نفترض ذلك $\{1,2,3,4,5,6\}$ هي إحدى المجموعات (وإلا قم بتبديل جميع الأرقام كما هي)، لذلك يمكنك تشفير هذه الحقيقة في مثيل SAT الخاص بك.كلما زاد عدد هذه الدروس التي يمكنك إثباتها، كان أداء اختبار SAT أفضل.

يمكنك أيضًا تشفير المجموعات بشكل مختلف.يترك $S_i$ تدل على $i$المجموعة التي يتم اختيارها بواسطة $\mathcal{S}$.إدخال المتغيرات $x_{i,j}$ للإشارة إلى ذلك $j \في S_i$ والمتغيرات $y_{i,A}$ للإشارة إلى أن $A \ مجموعة فرعية S_i $, ، لكل $A \subseteq \{1,\dots,17\}$ مع $|أ|=3$ وكل $i \في \{1,\dots,n\}$ وكل $j \في \{1,\dots,17\}$.أضف جملة $\bigvee_i y_{i,A}$ لكل $أ$ للتأكد من أن كل $أ$ يتم تغطيتها بمجموعة واحدة على الأقل.أضف قيدًا 6 من أصل 17 لكل منها $i$ للإشارة إلى أن بالضبط 6 من $x_{i,j}$هذا صحيح.وأخيرًا، أضف قيودًا لفرض الاتساق بين $x$'رمل $ص$'س.وعلى وجه الخصوص لكل $A=\{a_1,a_2,a_3\}$, ، إضافة فقرات $ eg x_{i,a_1} \lor eg x_{i,a_2} \lor eg x_{i,a_3} \lor y_{i,A}$ و $ eg y_{i,A} \lor x_{i,a_1}$ و $ eg y_{i,A} \lor x_{i,a_2}$ و $ eg y_{i,A} \lor x_{i,a_3}$.هذا سوف يتطلب حوالي $(17+680)ن$ المتغيرات و 4 دولارات \cdot 680 ن دولارًا الشروط (بدون احتساب $ن$ 6 قيود من أصل 17)؛منذ أن أتوقع $ن \حوالي 35 دولارًا, ، هذا حوالي 24 ألف متغير و100 ألف عبارة.هذه عبارات أكثر من ترميزك، ولها تناسق أكبر، لذلك قد يكون أداؤها أسوأ - على الرغم من أنها عبارات أقصر، ومن الصعب التنبؤ بالترميزات التي ستعمل بشكل أفضل مع SAT، لذلك غالبًا ما تكون هناك حاجة إلى بعض التجارب.

يمكنك أيضًا محاولة التعبير عن هذا كمثيل ILP بدلاً من SAT.