道場 · dojo
SAT 도장
SAT 솔버를 위한 체육관이에요. 솔버를 WebAssembly로 컴파일해 제출하면 비공개 새 논리식 세트로 채점돼요. 하시 퍼즐, 패리티 함정, 무작위 3-SAT, 비둘기집, 퀸.
리더보드 番付 · banzuke
논리식당 평균 연료(10억 단위)이며, 풀지 못한 논리식은 예산의 두 배로 계산해요. 낮을수록 좋아요.
불러오는 중…
진행 방식 稽古 · keiko
一만들기
WASI preview 1로 컴파일되는 언어라면 무엇이든 돼요: Rust, wasi-sdk를 쓴 C와 C++, Zig, Go. 표준 입력에서 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가 가장 낮은 솔버가 이겨요. 논리식당 평균 연료이며, 풀지 못한 논리식은 예산의 두 배로 계산해요.
논리식
하시
10×10부터 28×28까지의 하시 퍼즐을 연결성 규칙 없이 CNF로 바꾼 것이에요. 항상 충족 가능해요.
하시 패리티
숫자 하나를 바꿔 합이 홀수가 되게 한 퍼즐이에요. 다리는 항상 2씩 더하므로 충족 불가능해요. 보기엔 쉽지만 도출 원리(resolution)로 증명하기는 어려워요.
무작위 3-SAT
상전이 지점(변수당 절 4.26개)의 균일 무작위 3-SAT로, 약 절반이 충족 가능해요.
비둘기집
n개의 구멍에 n+1마리의 비둘기: 지수적으로 긴 도출 증명이 필요한 고전 문제예요. 딱 들어맞는 경우도 몇 개 섞었어요.
퀸
최대 48×48 판에서 몇몇 칸을 금지한 N퀸 문제예요.
도장에 입문하기 入門 · nyūmon
불러오는 중…
공정한 경쟁 礼 · rei
초가 아닌 연료
실행된 WebAssembly 명령어 하나당 연료 1단위, 벌크 메모리 연산은 바이트당 1단위가 들어요. 시계와 난수는 시드가 고정되어 있어, 솔버는 어느 기기에서든 언제나 같은 점수를 받아요.
비공개 새 논리식
테스트 세트는 시즌마다 바뀌는 비밀 시드에서 만들어지고, 모든 논리식은 뒤섞여요. 변수 이름 변경과 부정, 절 순서 섞기. 결과는 유형별로만 보여 주고 논리식별로는 절대 공개하지 않아요.
모든 답을 검증
모델은 논리식에 대해 검증돼요. UNSAT은 증명이 있을 때만 인정돼요. 비둘기집과 하시 패리티는 구성상 충족 불가능하고, 그 밖의 모든 UNSAT 라벨에는 저희 체커가 검증한 DRAT 증명이 붙어 있어요. 오답이 하나라도 있으면 실격이므로 찍기는 절대 통하지 않아요.
밀폐된 샌드박스
파일도, 네트워크도, 환경 변수도 없어요. 메모리와 출력은 제한되고, 제출물은 데이터가 전혀 없는 별도 서버에서 실행돼요.
계정 하나, 최고 기록 하나
계정은 만든 지 하루가 지나야 제출할 수 있고, 계정당 그리고 네트워크당 하루 세 번까지 제출할 수 있어요. 똑같은 코드는 이름을 바꾸거나 군더더기를 덧붙여도 거부되고, 가장 좋은 제출만 순위에 올라요.
복제 금지
점수가 정확하기 때문에 솔버는 지문을 남겨요. 바로 각 논리식에서 쓰는 연료예요. 다른 사람의 이전 제출과 똑같이 동작하는 제출은 순위에 오르지 않아요. 이를 피할 만큼 복제본을 고치면 그건 다른 솔버가 되고, 더 느리게 만들면 원본보다 아래로 갈 뿐이에요.
시즌
새 시즌이 시작되면 새 비공개 세트가 나오고 모든 제출물을 다시 평가해요.
연구자를 위해
연료는 결정적이라 결과를 재현할 수 있고 논문끼리 비교할 수 있어요. 시즌과 개발 시드를 밝혀 주세요. 리더보드는 /dojo/board.json에서 JSON으로 받을 수 있고, 평가 하네스는 오픈 소스예요.