道場 · dojo
SAT डोजो
SAT सॉल्वरों का जिम। अपना सॉल्वर WebAssembly में कंपाइल करें, जमा करें, और उसे नए फ़ॉर्मूलों के एक छिपे सेट पर स्कोर किया जाएगा: Hashi पहेलियाँ, पैरिटी जाल, रैंडम 3-SAT, कबूतर और रानियाँ।
लीडरबोर्ड 番付 · banzuke
हर फ़ॉर्मूले का औसत फ़्यूल, अरबों में; बिना हल हुए फ़ॉर्मूले बजट के दोगुने गिने जाते हैं। जितना कम, उतना बेहतर।
लोड हो रहा है…
यह कैसे काम करता है 稽古 · keiko
一बनाएँ
WASI preview 1 में कंपाइल होने वाली कोई भी भाषा चलेगी: Rust, wasi-sdk के साथ C और C++, Zig, Go। stdin से DIMACS पढ़ें और 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
10×10 से 28×28 तक की Hashiwokakero पहेलियाँ CNF के रूप में, कनेक्टिविटी नियम के बिना। हमेशा संतुष्ट करने योग्य।
Hashi पैरिटी
ऐसी पहेलियाँ जिनमें एक संख्या बदल दी गई है ताकि संख्याओं का योग विषम हो जाए। इन्हें संतुष्ट नहीं किया जा सकता, क्योंकि हर पुल दो जोड़ता है। देखना आसान, रेज़ोल्यूशन से साबित करना कठिन।
रैंडम 3-SAT
फ़ेज़ ट्रांज़िशन पर एकसमान रैंडम 3-SAT, प्रति वेरिएबल 4.26 क्लॉज़, इनमें से लगभग आधे संतुष्ट करने योग्य।
कबूतरखाना
n खानों में n+1 कबूतर: वह क्लासिक जिसके लिए घातांकीय रूप से लंबे रेज़ोल्यूशन प्रमाण चाहिए। साथ में कुछ ऐसे भी जिनमें कबूतर समा जाते हैं।
रानियाँ
48×48 तक के बोर्ड पर N रानियाँ, कुछ वर्जित खानों के साथ।
डोजो में प्रवेश करें 入門 · nyūmon
लोड हो रहा है…
निष्पक्ष खेल 礼 · rei
सेकंड नहीं, फ़्यूल
हर निष्पादित WebAssembly निर्देश की कीमत फ़्यूल की एक इकाई है, बल्क मेमोरी ऑपरेशन की प्रति बाइट एक। घड़ियाँ और रैंडम संख्याएँ तय सीड से चलती हैं, इसलिए सॉल्वर को हर मशीन पर, हर बार एक ही स्कोर मिलता है।
छिपे, नए फ़ॉर्मूले
टेस्ट सेट एक गुप्त सीड से बनता है जो हर सीज़न बदलता है, और हर फ़ॉर्मूला उलट-पुलट किया जाता है: वेरिएबल के नाम बदले और नकारे जाते हैं, क्लॉज़ फेंटे जाते हैं। नतीजे सिर्फ़ परिवार के हिसाब से दिखाए जाते हैं, कभी फ़ॉर्मूले के हिसाब से नहीं।
हर जवाब की जाँच
मॉडलों को फ़ॉर्मूले से मिलाकर सत्यापित किया जाता है। UNSAT सिर्फ़ वहीं गिना जाता है जहाँ हमारे पास प्रमाण हो: कबूतरखाना और Hashi पैरिटी अपनी बनावट से ही असंतोषणीय हैं, और हर दूसरे UNSAT लेबल के साथ एक DRAT प्रमाण होता है जिसे हमारे अपने चेकर ने सत्यापित किया है। एक भी गलत जवाब सबमिशन को अयोग्य कर देता है, इसलिए अंदाज़ा लगाने से कभी फ़ायदा नहीं होता।
सीलबंद सैंडबॉक्स
न फ़ाइलें, न नेटवर्क, न एनवायरनमेंट। मेमोरी और आउटपुट सीमित हैं, और सबमिशन एक अलग मशीन पर चलते हैं जिस पर कोई डेटा नहीं है।
एक खाता, सबसे अच्छी एंट्री
जमा करने के लिए खाता कम से कम एक दिन पुराना होना चाहिए, और हर खाते और हर नेटवर्क से दिन में तीन सबमिशन हो सकते हैं। एक जैसा कोड अस्वीकार किया जाता है, भले ही उसका नाम बदला गया हो या उसमें फ़ालतू डेटा जोड़ा गया हो, और सिर्फ़ आपके सबसे अच्छे सबमिशन को रैंक मिलती है।
कॉपी नहीं
स्कोर बिल्कुल सटीक होते हैं, इसलिए हर सॉल्वर एक फ़िंगरप्रिंट छोड़ता है: हर फ़ॉर्मूले पर खर्च किया गया उसका फ़्यूल। जो सबमिशन किसी और के पहले वाले सबमिशन जैसा व्यवहार करता है, उसे रैंक नहीं मिलती। किसी कॉपी को इतना बदलना कि वह इससे बच जाए, उसे एक अलग सॉल्वर बना देता है, और उसे धीमा करने से वह सिर्फ़ मूल से नीचे चली जाती है।
सीज़न
नया सीज़न नया छिपा सेट लाता है और हर सबमिशन का फिर से मूल्यांकन होता है।
शोधकर्ताओं के लिए
फ़्यूल नियतात्मक है, इसलिए नतीजे दोहराए जा सकते हैं और शोधपत्रों के बीच तुलनीय हैं: सीज़न और डेव सीड बताएँ। लीडरबोर्ड /dojo/board.json पर JSON के रूप में उपलब्ध है, और हार्नेस ओपन सोर्स है।