道場 · dojo
โดโจ SAT
ยิมสำหรับตัวแก้ SAT คอมไพล์ตัวแก้ของคุณเป็น WebAssembly แล้วส่งมา มันจะถูกวัดผลบนชุดสูตรใหม่ที่ซ่อนไว้: ปริศนา Hashi กับดักพาริตี 3-SAT แบบสุ่ม นกพิราบ และควีน
ตารางอันดับ 番付 · banzuke
ค่าเฉลี่ย fuel ต่อสูตร หน่วยพันล้าน สูตรที่แก้ไม่ได้นับเป็นสองเท่าของงบ ยิ่งต่ำยิ่งดี
กำลังโหลด…
ทำงานอย่างไร 稽古 · 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二ฝึก
วัดผลตัวแก้บนเครื่องของคุณเองกับชุด dev สาธารณะด้วยเครื่องมือ 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 ต่ำสุดชนะ: ค่าเฉลี่ย fuel ต่อสูตร โดยสูตรที่แก้ไม่ได้นับเป็นสองเท่าของงบ
สูตรต่างๆ
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
fuel ไม่ใช่วินาที
คำสั่ง WebAssembly ทุกคำสั่งที่ถูกรันใช้ fuel หนึ่งหน่วย การดำเนินการหน่วยความจำแบบ bulk ใช้หนึ่งหน่วยต่อไบต์ นาฬิกาและตัวเลขสุ่มใช้ seed คงที่ ตัวแก้จึงได้คะแนนเท่าเดิมบนทุกเครื่อง ทุกครั้ง
สูตรใหม่ที่ซ่อนไว้
ชุดทดสอบสร้างจาก seed ลับที่เปลี่ยนทุกฤดูกาล และทุกสูตรถูกสับเปลี่ยน: ตัวแปรถูกเปลี่ยนชื่อและกลับค่า อนุประโยคถูกสลับลำดับ ผลลัพธ์แสดงเป็นรายตระกูลเท่านั้น ไม่เคยแสดงรายสูตร
ตรวจทุกคำตอบ
โมเดลทุกตัวถูกตรวจกับสูตร UNSAT จะนับเฉพาะเมื่อเรามีบทพิสูจน์ รังนกพิราบและ Hashi พาริตีทำให้เป็นจริงไม่ได้ตามวิธีสร้าง ส่วนป้าย UNSAT อื่นทุกป้ายมาพร้อมบทพิสูจน์ DRAT ที่ตัวตรวจของเราเองยืนยันแล้ว คำตอบผิดเพียงข้อเดียวทำให้ผลงานที่ส่งถูกตัดสิทธิ์ การเดาจึงไม่มีวันคุ้ม
แซนด์บ็อกซ์ปิดผนึก
ไม่มีไฟล์ ไม่มีเครือข่าย ไม่มีตัวแปรสภาพแวดล้อม หน่วยความจำและเอาต์พุตถูกจำกัด และผลงานที่ส่งทั้งหมดรันบนเครื่องแยกที่ไม่มีข้อมูลใดๆ
หนึ่งบัญชี ผลงานดีที่สุด
บัญชีต้องมีอายุครบหนึ่งวันจึงจะส่งได้ และส่งได้วันละสามครั้งต่อบัญชีและต่อเครือข่าย โค้ดที่เหมือนกันจะถูกปฏิเสธ แม้จะเปลี่ยนชื่อหรือเติมข้อมูลส่วนเกินเข้าไป และจัดอันดับเฉพาะผลงานที่ดีที่สุดของคุณ
ห้ามลอกเลียน
คะแนนแม่นยำ ตัวแก้จึงทิ้งลายนิ้วมือไว้ นั่นคือ fuel ที่ใช้ในแต่ละสูตร ผลงานที่ทำงานเหมือนผลงานก่อนหน้าของคนอื่นจะไม่ถูกจัดอันดับ การแก้สำเนามากพอจะหลบเลี่ยงได้ก็ทำให้มันกลายเป็นตัวแก้อีกตัวหนึ่ง และการทำให้ช้าลงก็แค่ทำให้มันอยู่ต่ำกว่าต้นฉบับ
ฤดูกาล
ฤดูกาลใหม่มาพร้อมชุดซ่อนชุดใหม่ และผลงานที่ส่งทั้งหมดจะถูกประเมินใหม่
สำหรับนักวิจัย
fuel ให้ผลแน่นอน ผลลัพธ์จึงทำซ้ำได้และเทียบกันได้ระหว่างงานวิจัย: ระบุฤดูกาลและ seed ของชุด dev ตารางอันดับมีให้ในรูป JSON ที่ /dojo/board.json และ harness เป็นโอเพนซอร์ส