道場 · dojo
دوجو SAT
صالة تدريب لحلّالات SAT. صرّف حلّالك إلى WebAssembly وأرسله، فيُقيَّم على مجموعة مخفية من الصيغ الجديدة: ألغاز Hashi، وفخاخ التكافؤ، وصيغ 3-SAT عشوائية، والحمام والملكات.
لوحة الصدارة 番付 · banzuke
متوسط الوقود لكل صيغة بالمليارات، والصيغ غير المحلولة تُحتسب بضعف الميزانية. الأقل أفضل.
جارٍ التحميل…
كيف يعمل 稽古 · keiko
一ابنِ
تصلح أي لغة تُصرَّف إلى WASI preview 1: Rust، وC وC++ مع wasi-sdk، وZig، وGo. اقرأ DIMACS من stdin وأجب كما في مسابقة SAT.
$ cargo build --release --target wasm32-wasip1
stdin p cnf 3 2
1 -2 0
2 3 0
stdout s SATISFIABLE
v 1 2 -3 0二تدرّب
قيّم حلّالك محليًا على مجموعة التطوير العامة بأداة dojo. تعمل تمامًا مثل لوحة الصدارة، فتعرف نتيجتك قبل أن ترسل.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三أرسل
ارفع ملف .wasm. يعمل على المجموعة المخفية للموسم الحالي، على جهازنا الخاص.
四تسلّق
يفوز صاحب أدنى PAR-2: متوسط الوقود لكل صيغة، حيث تُحتسب الصيغ غير المحلولة بضعف الميزانية.
الصيغ
Hashi
ألغاز Hashiwokakero من 10×10 إلى 28×28 بصيغة CNF، دون قاعدة الاتصال. قابلة للإرضاء دائمًا.
تكافؤ Hashi
ألغاز غُيِّر فيها رقم واحد ليصبح مجموع الأرقام فرديًا. غير قابلة للإرضاء، لأن كل جسر يضيف اثنين. يسهل رؤية ذلك، ويصعب إثباته بقاعدة الحلّ (resolution).
3-SAT عشوائي
صيغ 3-SAT عشوائية منتظمة عند نقطة التحوّل الطوري، بنسبة 4.26 بين البنود والمتغيرات، ونحو نصفها قابل للإرضاء.
برج الحمام
حمام عدده n+1 في أعشاش عددها n: المسألة الكلاسيكية التي تتطلب براهين resolution طويلة طولًا أسّيًا. ومعها بعض الحالات التي يتسع فيها الحمام.
الملكات
ملكات عددها N على رقع حتى 48×48 مع بضعة مربعات محظورة.
ادخل الدوجو 入門 · nyūmon
جارٍ التحميل…
اللعب النظيف 礼 · rei
وقود لا ثوانٍ
كل تعليمة WebAssembly منفَّذة تكلّف وحدة وقود واحدة، وعمليات الذاكرة الجماعية وحدة لكل بايت. الساعات والأعداد العشوائية مُهيّأة ببذرة ثابتة، فيحصل الحلّال على النتيجة نفسها على كل جهاز وفي كل مرة.
صيغ مخفية وجديدة
تأتي مجموعة الاختبار من بذرة سرية تتغير كل موسم، وكل صيغة مخلوطة: المتغيرات مُعادة التسمية ومنفيّة، والبنود مبعثرة الترتيب. تُعرض النتائج لكل عائلة فقط، ولا تُعرض لكل صيغة أبدًا.
كل إجابة تُفحص
يُتحقق من النماذج مقابل الصيغة. لا تُحتسب UNSAT إلا حيث لدينا برهان: برج الحمام وتكافؤ Hashi غير قابلين للإرضاء بحكم بنائهما، وكل تصنيف UNSAT آخر يرافقه برهان DRAT تحقق منه مدقّقنا الخاص. إجابة خاطئة واحدة تُقصي الإرسال، فالتخمين لا يجدي أبدًا.
بيئة معزولة محكمة
لا ملفات، ولا شبكة، ولا متغيرات بيئة. الذاكرة والمخرجات محدودة، وتعمل الإرسالات على جهاز منفصل لا يحمل أي بيانات.
حساب واحد، أفضل مشاركة
يجب أن يكون عمر الحساب يومًا واحدًا على الأقل ليتمكن من الإرسال، والحد ثلاثة إرسالات يوميًا لكل حساب ولكل شبكة. تُرفض الشيفرة المتطابقة حتى لو أُعيدت تسميتها أو حُشيت ببيانات زائدة، ولا يدخل الترتيب إلا أفضل إرسال لك.
لا للنسخ
النتائج دقيقة، لذا يترك الحلّال بصمة: الوقود الذي يستهلكه على كل صيغة. الإرسال الذي يتصرف مثل إرسال سابق لشخص آخر لا يدخل الترتيب. تعديل النسخة بما يكفي للإفلات من ذلك يجعلها حلّالًا مختلفًا، وجعلها أبطأ لا يفعل سوى وضعها تحت الأصل.
المواسم
يأتي كل موسم جديد بمجموعة مخفية جديدة، ويُعاد تقييم كل الإرسالات.
للباحثين
الوقود حتمي، لذا النتائج قابلة للتكرار وللمقارنة بين الأوراق البحثية: اذكر الموسم وبذرة مجموعة التطوير. لوحة الصدارة متاحة بصيغة JSON على /dojo/board.json، وأداة التقييم مفتوحة المصدر.