gophersat
1.0.0
هذا هو Gophersat، وهو اختبار SAT وحلال منطقي زائف مكتوب بلغة Go فقط. تم تطوير Gophersat بواسطة CRIL (Centre de Recherche en Informatique de Lens) في جامعة أرتوا والمركز الوطني الفرنسي للبحوث العلمية. تم إصداره بموجب ترخيص MIT. يعد Gophersat فعالا إلى حد ما، أي أنه في معايير SAT النموذجية يعمل بشكل أبطأ بنحو 2 إلى 5 مرات من أجهزة الحل ذات المستوى الأعلى (أي الجلوكوز أو minisat) التي مستوحى منها بقوة. ويمكنه أيضًا حل مشكلات MAXSAT ومشاكل القرار والتحسين المنطقية الزائفة.
آخر إصدار مستقر لـ Gophersat هو الإصدار 1.4. يتضمن استراتيجية حل طائرات القطع الاختيارية.
بعض المسائل، مثل مسألة التصنيف الشهيرة، تستغرق وقتًا طويلاً جدًا لحلها باستخدام التفكير المنطقي البحت.
يمكن التعبير عن مشكلة الحمام بهذه الطريقة: هل من الممكن وضع n الحمام في m الحمام، حيث m = n-1، دون وضع عدة حمامات في نفس الحفرة ووضع كل الحمام في حفرة؟ الجواب واضح: إذا كان لديك 4 حمامات في 3 حفر، فلا يمكنك وضعهم جميعًا في حفرة مختلفة. ولكن كيف تثبت هذا؟ سيثبت حل SAT أو PB ذلك من خلال تجربة جميع المجموعات الممكنة، وسيزداد عدد المجموعات الممكنة بشكل كبير. لذا، فإن محاولة حل المشكلة باستخدام n=20 غير ممكنة عمليًا، على الرغم من أن المشكلة لها إجابة واضحة.
ينفذ بعض محللي PB إستراتيجية بديلة: إستراتيجية طائرات القطع. لن يتم وصفها بالتفصيل في هذه الوثيقة، ولكن يمكن أن تكون هذه الإستراتيجية فعالة للغاية في بعض المشكلات، مثل مشكلة التصنيف التي لا يمكن حلها بكفاءة عن طريق التفكير المنطقي البحت، ولكنها ستكون أبطأ في معظم المشكلات.
أصبح من الممكن الآن استخدام طائرات القطع مع Gophersat. ما عليك سوى استخدام خيار سطر الأوامر -cp . لذا، بدلاً من الاتصال:
gophersat problem.opb
فقط اتصل:
gophersat -cp problem.opb
آخر إصدار مستقر لـ Gophersat هو الإصدار 1.3. إنه تحديث بسيط، يضيف القدرة على الوصول إلى الحل الأساسي عند التعامل مع مشكلات MAXSAT.
يتضمن Gophersat الإصدار 1.2 طريقة لفهم مثيلات UNSAT، سواء من خلال توفير شهادات RUP عندما تكون المشكلة هي UNSAT أو من خلال توفير القدرة على استخراج مجموعات فرعية غير مرضية من الصيغة. تم أيضًا تصحيح عدد من الأخطاء، كما تم تحسين دعم حل اختبار SAT المتزايد.
لمعرفة المزيد حول هذه الوظائف، يمكنك مراجعة البرنامج التعليمي حول شهادات UNSAT وMUSes.
لإنشاء شهادة باستخدام gophersat القابل للتنفيذ، ما عليك سوى الاتصال بـ:
gophersat -certified problem.cnf
سيتم بعد ذلك طباعة الشهادة على الإخراج القياسي، باستخدام تدوين RUP. يتم إنشاء الشهادة بسرعة، لذا انتبه إلى أنه سيتم إنشاء شهادة جزئية وغير مجدية حتى لو كانت المشكلة مرضية بالفعل. هذه ممارسة شائعة في المجتمع، وعلى الرغم من أن الجمل التي تم إنشاؤها هي ضوضاء عديمة الفائدة، إلا أن هذه ليست مشكلة في الممارسة العملية.
لاستخراج MUS من مثيل UNSAT، ما عليك سوى الاتصال بـ:
gophersat -mus problem.cnf
سيتم طباعة MUS على الإخراج القياسي. إذا كانت المشكلة ليست UNSAT، فسيتم عرض رسالة خطأ.
في الوقت الحالي، تتوفر هذه المرافق فقط لمشاكل SAT الخالصة (أي ليست مشاكل منطقية زائفة).
منذ الإصدار 1.1، يشتمل Gophersat على حل أساسي جديد وأكثر كفاءة لمشاكل SAT الخالصة وحزمة تتعامل مع مشاكل MAXSAT. ويتضمن أيضًا واجهة برمجة تطبيقات جديدة للتحسين وإحصاء النماذج، حيث تتم كتابة النماذج الجديدة على القنوات بمجرد العثور عليها.
منذ الإصدار 1.0، تعتبر واجهة برمجة التطبيقات الخاصة بـ Gophersat مستقرة، مما يعني أن واجهة برمجة التطبيقات مضمونة للبقاء متوافقة مع الإصدارات السابقة حتى يتم تغيير الإصدار الرئيسي. بمعنى آخر، إذا كان برنامجك يعمل مع الإصدار 1.0 من gophersat، فسيظل يعمل مع الإصدار 1.1 أو أعلى، ولكن ليس بالضرورة مع الإصدارات الأعلى من 2.0.
لاحظ أنه عندما نقول "الاستمرار في العمل"، فإننا نعني فقط "سوف نقوم بتجميع وإنتاج نفس المخرجات"، وليس "سيكون لها نفس الأداء من حيث الذاكرة أو الوقت". يعد هذا تمييزًا مهمًا: أثناء ترقيات الإصدار البسيطة، يمكن تقديم أساليب استدلالية أو أنواع بيانات جديدة، مما يعني أنه يمكن حل بعض المشكلات المحددة بشكل أسرع أو أبطأ من السابق.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
يمكن استخدام Gophersat كحل مستقل (قراءة ملفات DIMACS CNF) أو كمكتبة في أي برنامج Go.
لحل ملف DIMACS، يمكنك الاتصال بـ gophersat باستخدام الصيغة التالية:
gophersat --verbose file.cnf
حيث --verbose عبارة عن معلمات اختيارية تجعل الحل يعرض المعلومات أثناء عملية الحل.
يستطيع Gophersat أيضًا قراءة وحل الصيغ المنطقية الأكثر عمومية، وليس فقط المشكلات الممثلة في تنسيق DIMACS غير السهل الاستخدام. كما أنه يتعامل أصلاً مع القيود الأساسية، أي الجمل التي يجب أن تحتوي على الأقل على n من القيم الحرفية الصحيحة، مع n > 1.
يمكن استخدام Gophersat كحل مستقل (قراءة ملفات OPB) أو كمكتبة في أي برنامج go.
لحل مشكلة منطقية زائفة (سواء كانت قرارًا واحدًا أو قرارًا مثاليًا)، يمكنك الاتصال بـ gophersat باستخدام الصيغة التالية:
gophersat --verbose file.opb
حيث --verbose عبارة عن معلمات اختيارية تجعل الحل يعرض المعلومات أثناء عملية الحل.
في الوقت الحالي، يمكنها فقط حل ما يسمى بمشاكل DEC-SMALLINT-LIN وOPT-SMALLINT-LIN، أي مشاكل القرار (هل هناك حل أم لا)، للقيود الخطية (مجموع القيم الحرفية الموزونة) على الأعداد الصحيحة الصغيرة (n < 2^30)، أو مشاكل التحسين (ما هو الحل الأفضل، تقليل دالة تكلفة معينة)، للقيود الخطية على الأعداد الصحيحة الصغيرة.
بفضل حزمة maxsat ، يستطيع Gophersat الآن حل مشاكل MAXSAT.
لحل مشكلة MAXSAT الموزونة، يمكنك الاتصال بـ gophersat باستخدام الصيغة التالية:
gophersat --verbose file.wcnf
حيث --verbose عبارة عن معلمات اختيارية تجعل الحل يعرض المعلومات أثناء عملية الحل. من المفترض أن يتم تمثيل الملف بـ (تنسيق WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT، الذي يرمز إلى مشكلة الرضا المنطقية ، هو مشكلة NP-Complete الأساسية، أي مشكلة لا يوجد لها حل معروف ولا تستغرق وقتًا أسيًا في الحالة الأسوأ. في بضع كلمات، يحاول محلل SAT العثور، بالنسبة لصيغة افتراضية معينة، على تعيين لجميع متغيراتها التي تجعلها صحيحة، إذا كان هذا التعيين موجودًا.
في حين أنه من التافه تنفيذ حل SAT باستخدام خوارزمية ساذجة، فإن مثل هذا التنفيذ سيكون غير فعال للغاية في الممارسة العملية. يستخدم Gophersat أحدث الميزات وبالتالي فهو فعال للغاية، مما يجعله قابلاً للاستخدام عمليًا في برامج Go التي تحتاج إلى محرك استدلال فعال.
على الرغم من أن هذا ليس دائمًا القرار الأفضل لأسباب عملية، إلا أنه يمكن ترجمة أي مشكلة NP-Complete إلى مشكلة SAT وحلها بواسطة Gophersat. تتضمن هذه المشكلات مشكلة البائع المتجول، وبرمجة القيود، ومشكلة حقيبة الظهر، والتخطيط، والتحقق من النماذج، والتحقق من صحة البرامج، وما إلى ذلك.
يمكن العثور على المزيد حول مشكلة SAT في مقالة ويكيبيديا حول SAT.
يمكنك أيضًا العثور على معلومات حول كيفية تمثيل الصيغ المنطقية الخاصة بك حتى يمكن استخدامها بواسطة gophersat في البرنامج التعليمي "SAT for noobs".
MAXSAT هو المعادل الأمثل لمشكلة قرار SAT. في حين أن حل SAT الخالص سيعيد إما نموذجًا يلبي جميع البنود أو UNSAT في حالة عدم وجود مثل هذا النموذج، فإن حل MAXSAT سيعيد نموذجًا يفي بأكبر عدد ممكن من البنود.
هناك امتدادات لـ MAXSAT.
يعني MAXSAT الجزئي أنه على الرغم من أننا نريد تلبية أكبر عدد ممكن من البنود، إلا أن بعض البنود (وتسمى البنود الصلبة ) يجب استيفاؤها، بغض النظر عن السبب. وبالتالي يمكن اعتبار مشكلة MAXSAT جزئية غير مرضية.
على سبيل المثال، يعد إنشاء جدول زمني للمدرسة مشكلة جزئية لـ MAXSAT: هناك مشكلة بسيطة (نريد أن يكون لدينا أقل عدد ممكن من الفصول الدراسية التي تبدأ بعد الساعة 4 مساءً، على سبيل المثال) وصعبة (لا يمكن أن يكون مدرسان في مكانين مختلفين في في نفس الوقت) القيود.
يعني MAXSAT المرجح أن البنود مرتبطة بالتكلفة: على الرغم من أنها اختيارية، إلا أن بعض البنود تعتبر أكثر أهمية من غيرها. على سبيل المثال، إذا كان البند C1 له تكلفة 3 والبندان C2 وC3 كلاهما لهما تكلفة 1، فإن الحل الذي يرضي C1 ولكن لا C2 أو C3 سيتم اعتباره أفضل من الحل الذي يرضي كلاً من C2 وC3 ولكن ليس C1، وجميع الحلول الأخرى الأمور متساوية.
يعني MAXSAT المرجح جزئيًا أن هناك بنودًا ناعمة وصعبة في المشكلة، ويتم ترجيح البنود الناعمة. في هذا الصدد، تعد مشكلة MAXSAT "الخالصة" حالة خاصة من MAXSAT الموزونة جزئيًا الأكثر عمومية: مشكلة MAXSAT "الخالصة" هي مشكلة MAXSAT جزئية مرجحة حيث تكون جميع البنود عبارة عن جمل ناعمة مرتبطة بوزن 1.
تعد المسائل المنطقية الزائفة، بطريقة ما، تعميمًا لمشكلات SAT: يمكن كتابة أي جملة افتراضية كقيد منطقي زائف واحد، ولكن تمثيل قيد منطقي زائف يمكن أن يتطلب عددًا أسيًا من الجمل الافتراضية.
التعبير المنطقي الزائف (الخطي) هو تعبير مثل:
w1 l1 + w2 x2 + ... + wn xn ≥ y
حيث y و all wi عبارة عن ثوابت عددية وكل li عبارة عن قيم حرفية منطقية.
على سبيل المثال، ليكون التعبير التالي صحيحا
2 ¬x1 + x2 + x3 ≥ 3
يجب أن يكون المتغير المنطقي x1 خطأ، ويجب أن يكون واحد على الأقل من x2 و x3 صحيحًا. وهذا يعادل الصيغة المقترحة
¬x1 ∧ (x2 ∨ x3)
التعبيرات المنطقية الزائفة هي تعميم للبنود الافتراضية: أي جملة
x1 ∨ x2 ∨ ... ∨ xn
يمكن إعادة كتابتها كما
x1 + x2 + ... + xn ≥ 1
يمكن أن يكون وصف المشكلة المنطقية الزائفة أصغر بشكل كبير من نظيرتها الافتراضية، ولكن حل المشكلة المنطقية الزائفة لا يزال مكتملًا بـ NP.
يقوم Gophersat بحل مشاكل القرار (هل يوجد حل للمشكلة على الإطلاق)، ومشكلة التحسين. مشكلة التحسين هي مشكلة منطقية زائفة مرتبطة بوظيفة التكلفة، أي مجموع المصطلحات التي يجب تقليلها إلى الحد الأدنى. بدلاً من مجرد محاولة العثور على نموذج يلبي القيود المعطاة، سيحاول gophersat بعد ذلك العثور على نموذج يضمن تلبية القيود وتقليل دالة التكلفة.
أثناء البحث عن تلك الحلول المثالية، ستوفر gophersat حلولاً دون المستوى الأمثل (أي الحلول التي تحل جميع القيود ولكن ليس من المضمون بعد أن تكون مثالية) بمجرد العثور عليها، بحيث يمكن للمستخدم إما الحصول على حل دون المستوى الأمثل في وقت معين الحد، أو الانتظار لفترة أطول للحصول على الحل الأمثل المضمون.
نعم ولا. إنه أسرع بكثير من التطبيقات الساذجة، وسريع بما يكفي لاستخدامه في حل مشكلات العالم الحقيقي، ولكنه أبطأ من أدوات الحل عالية المستوى والمُحسّنة للغاية والمتطورة.
لا يهدف Gophersat إلى أن يكون أسرع حل متاح لـSAT/PB. الهدف هو منح الوصول إلى تقنيات SAT وPB للغوفر، دون اللجوء إلى واجهات للحلول المكتوبة بلغات أخرى (عادةً C/C++).
ومع ذلك، في بعض الحالات، يكون التواصل مع أحد الحلول المكتوبة بلغة أخرى هو الخيار الأفضل لتطبيقك. إذا كان لديك الكثير من المشاكل الصغيرة التي تحتاج إلى حلها، فسيكون Gophersat هو البديل الأسرع. بالنسبة للمشكلات الأكبر، إذا كنت تريد أن يكون لديك أقل قدر ممكن من التبعيات على حساب حل الوقت، فإن Gophersat جيد أيضًا. إذا كنت بحاجة إلى حل المشكلات الصعبة ولا تمانع في استخدام cgo أو استخدام برنامج خارجي، فربما لا يكون Gophersat هو الخيار الأفضل.
هناك عدد قليل من حلول SAT الأخرى في Go، بشكل أساسي go-sat وgini. أداء Gini يتساوى إلى حد كبير مع Gophersat، على الرغم من أنه أبطأ قليلاً في المتوسط، وفقًا للاختبارات التي أجريناها.
يوفر Gophersat أيضًا ميزات رائعة لا تتوفر دائمًا مع أدوات الحل الأخرى (تنسيق إدخال سهل الاستخدام، على سبيل المثال)، لذا يمكن استخدامه كأداة لوصف وحل المشكلات الصعبة NP التي يمكن اختصارها بسهولة إلى SAT/PB مشكلة.
لا. توفر حزمة bf (لـ "الصيغة المنطقية") تسهيلات لترجمة أي صيغة منطقية إلى CNF.
يُعرف هذا باسم عد النماذج، ونعم، هناك وظيفة لذلك: solver.Solver.CountModels .
يمكنك أيضًا حساب النماذج من سطر الأوامر باستخدام
gophersat --count filename
حيث يمكن أن يكون اسم الملف ملف .opb أو ملف .cnf.
