道場 · dojo
Dojo SAT
Phòng tập cho các bộ giải SAT. Biên dịch bộ giải của bạn sang WebAssembly, gửi lên, và nó được chấm điểm trên một tập ẩn gồm các công thức mới: câu đố Hashi, bẫy chẵn lẻ, 3-SAT ngẫu nhiên, chim bồ câu và quân hậu.
Bảng xếp hạng 番付 · banzuke
Fuel trung bình mỗi công thức, tính bằng tỷ; công thức chưa giải được tính gấp đôi ngân sách. Càng thấp càng tốt.
Đang tải…
Cách hoạt động 稽古 · keiko
一Xây dựng
Mọi ngôn ngữ biên dịch được sang WASI preview 1 đều dùng được: Rust, C và C++ với wasi-sdk, Zig, Go. Đọc DIMACS từ stdin và trả lời như trong cuộc thi 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二Luyện tập
Chấm điểm bộ giải ngay trên máy của bạn với tập dev công khai bằng công cụ dojo. Nó chạy y hệt bảng xếp hạng, nên bạn biết điểm của mình trước khi gửi.
$ cargo install --git https://github.com/
NoelHuibers/Hashiwokakero dojo --features worker
$ dojo run my-solver.wasm
solved 26/34 PAR-2 4.855 Gfuel三Gửi
Tải lên tệp .wasm. Tệp sẽ chạy trên tập ẩn của mùa hiện tại, trên máy của chúng tôi.
四Leo hạng
PAR-2 thấp nhất thắng: fuel trung bình mỗi công thức, trong đó công thức chưa giải được tính gấp đôi ngân sách.
Các công thức
Hashi
Câu đố Hashiwokakero từ 10×10 đến 28×28 dưới dạng CNF, bỏ quy tắc liên thông. Luôn thỏa mãn được.
Hashi chẵn lẻ
Câu đố bị đổi một con số để tổng các số là số lẻ. Không thỏa mãn được, vì mỗi cây cầu cộng thêm hai. Dễ thấy, nhưng khó chứng minh bằng phép hợp giải (resolution).
3-SAT ngẫu nhiên
3-SAT ngẫu nhiên đều tại điểm chuyển pha, 4,26 mệnh đề mỗi biến, khoảng một nửa thỏa mãn được.
Chuồng bồ câu
n+1 con bồ câu trong n cái chuồng: bài toán kinh điển cần chứng minh hợp giải dài theo hàm mũ. Thêm vài bài vừa đủ chỗ.
Quân hậu
N quân hậu trên bàn cờ đến 48×48 với vài ô bị cấm.
Bước vào dojo 入門 · nyūmon
Đang tải…
Chơi đẹp 礼 · rei
Fuel, không phải giây
Mỗi lệnh WebAssembly được thực thi tốn một đơn vị fuel, thao tác bộ nhớ khối tốn một đơn vị mỗi byte. Đồng hồ và số ngẫu nhiên đều có seed cố định, nên một bộ giải luôn đạt cùng điểm trên mọi máy, mọi lần chạy.
Công thức ẩn và mới
Tập kiểm thử sinh từ một seed bí mật thay đổi mỗi mùa, và mọi công thức đều bị xáo trộn: biến được đổi tên và phủ định, mệnh đề bị trộn thứ tự. Kết quả chỉ hiện theo từng họ, không bao giờ theo từng công thức.
Mọi câu trả lời đều được kiểm tra
Mô hình được kiểm chứng với công thức. UNSAT chỉ được tính khi chúng tôi có chứng minh: chuồng bồ câu và Hashi chẵn lẻ không thỏa mãn được ngay từ cách xây dựng, mọi nhãn UNSAT khác đều kèm một chứng minh DRAT đã được bộ kiểm tra của chính chúng tôi xác minh. Chỉ một câu trả lời sai là bài gửi bị loại, nên đoán mò không bao giờ có lợi.
Hộp cát kín
Không tệp, không mạng, không biến môi trường. Bộ nhớ và đầu ra bị giới hạn, và bài gửi chạy trên một máy riêng không chứa dữ liệu nào.
Một tài khoản, bài tốt nhất
Tài khoản phải được tạo ít nhất một ngày mới được gửi bài, và mỗi tài khoản cũng như mỗi mạng được gửi ba bài mỗi ngày. Mã giống hệt bị từ chối, kể cả khi đổi tên hay chèn thêm phần đệm, và chỉ bài gửi tốt nhất của bạn được xếp hạng.
Không sao chép
Điểm số là chính xác, nên một bộ giải để lại dấu vân tay: lượng fuel nó dùng trên từng công thức. Bài gửi hoạt động giống một bài gửi trước đó của người khác sẽ không được xếp hạng. Sửa một bản sao đủ nhiều để thoát khỏi điều đó thì nó đã là một bộ giải khác, còn làm nó chậm đi chỉ đẩy nó xuống dưới bản gốc.
Các mùa
Mùa mới mang đến tập ẩn mới và mọi bài gửi được chấm lại.
Cho nhà nghiên cứu
Fuel là tất định, nên kết quả tái lập được và so sánh được giữa các bài báo: hãy ghi rõ mùa và seed dev. Bảng xếp hạng có sẵn dạng JSON tại /dojo/board.json, bộ chấm (harness) là mã nguồn mở.