道場 · dojo
SAT Dojo
SAT çözücüleri için bir spor salonu. Çözücünü WebAssembly'ye derle, gönder; gizli ve yeni formüllerden oluşan bir sette puanlansın: Hashi bulmacaları, parite tuzakları, rastgele 3-SAT, güvercinler ve vezirler.
Sıralama 番付 · banzuke
Formül başına milyar cinsinden ortalama yakıt; çözülemeyen formüller bütçenin iki katı sayılır. Düşük olan daha iyidir.
Yükleniyor…
Nasıl çalışır 稽古 · keiko
一Derle
WASI preview 1'e derlenen her dil olur: Rust, wasi-sdk ile C ve C++, Zig, Go. DIMACS'i stdin'den oku ve SAT Competition'daki gibi cevap ver.
$ 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二Antrenman
Çözücünü dojo aracıyla açık geliştirme setinde yerel olarak puanla. Sıralamayla birebir aynı şekilde çalışır, yani göndermeden önce puanını bilirsin.
$ 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önder
.wasm dosyasını yükle. Mevcut sezonun gizli setinde, kendi makinemizde çalıştırılır.
四Yüksel
En düşük PAR-2 kazanır: formül başına ortalama yakıt; çözülemeyen formüller bütçenin iki katı sayılır.
Formüller
Hashi
10×10'dan 28×28'e kadar Hashiwokakero bulmacaları CNF olarak, bağlantılılık kuralı olmadan. Her zaman sağlanabilir.
Hashi parite
Bir sayısı değiştirilerek sayıların toplamı tek yapılmış bulmacalar. Her köprü toplama iki eklediği için sağlanamaz. Görmesi kolay, rezolüsyonla kanıtlaması zor.
Rastgele 3-SAT
Faz geçişinde düzgün rastgele 3-SAT, değişken başına 4,26 tümce; yaklaşık yarısı sağlanabilir.
Güvercin yuvası
n yuvada n+1 güvercin: üstel uzunlukta rezolüsyon kanıtları gerektiren klasik. Artı güvercinlerin sığdığı birkaç örnek.
Vezirler
48×48'e kadar tahtalarda, birkaç yasak kareyle N vezir.
Dojoya gir 入門 · nyūmon
Yükleniyor…
Adil oyun 礼 · rei
Saniye değil, yakıt
Çalıştırılan her WebAssembly komutu bir birim yakıt harcar, toplu bellek işlemleri bayt başına bir birim. Saatler ve rastgele sayılar sabit tohumludur, böylece bir çözücü her makinede, her seferinde aynı puanı alır.
Gizli, yeni formüller
Test seti her sezon değişen gizli bir tohumdan üretilir ve her formül karıştırılır: değişkenler yeniden adlandırılır ve olumsuzlanır, tümcelerin sırası karıştırılır. Sonuçlar formül bazında değil, yalnızca aile bazında gösterilir.
Her cevap kontrol edilir
Modeller formüle karşı doğrulanır. UNSAT yalnızca bir kanıtımız olduğunda geçerlidir: güvercin yuvası ve Hashi parite yapıları gereği sağlanamazdır, diğer her UNSAT etiketi kendi denetleyicimizin doğruladığı bir DRAT kanıtıyla gelir. Tek bir yanlış cevap gönderimi diskalifiye eder, yani tahmin etmek asla işe yaramaz.
Kapalı bir korumalı alan
Dosya yok, ağ yok, ortam değişkeni yok. Bellek ve çıktı sınırlıdır ve gönderimler hiçbir veri tutmayan ayrı bir makinede çalışır.
Tek hesap, en iyi gönderim
Gönderim yapmak için hesapların en az bir günlük olması gerekir ve hesap başına ve ağ başına günde üç gönderim hakkı vardır. Aynı kod, yeniden adlandırılsa veya dolgu eklense bile reddedilir ve yalnızca en iyi gönderimin sıralamaya girer.
Kopya yok
Puanlar kesindir, bu yüzden bir çözücü parmak izi bırakır: her formülde harcadığı yakıt. Başka birinin daha önceki bir gönderimi gibi davranan bir gönderim sıralamaya girmez. Bir kopyayı bundan kurtulacak kadar değiştirmek onu farklı bir çözücü yapar, yavaşlatmak ise onu yalnızca orijinalin altına düşürür.
Sezonlar
Yeni bir sezon yeni bir gizli set getirir ve tüm gönderimler yeniden değerlendirilir.
Araştırmacılar için
Yakıt deterministiktir, bu yüzden sonuçlar tekrarlanabilir ve makaleler arasında karşılaştırılabilir: sezonu ve geliştirme setinin tohumunu belirt. Sıralama /dojo/board.json adresinde JSON olarak mevcut, test düzeneği açık kaynak.