研究室 · kenkyūshitsu
แล็บตัวแก้
ให้ตัวแก้ CDCL และ DPLL ของเราแข่งกันแก้ปริศนาข้อเดียวในโหมดต่างๆ (ฮิวริสติกการแตกกิ่ง นโยบายรีสตาร์ต ซับซัมชัน) แล้วเทียบกับ splr
3 · ผลลัพธ์ 結果
เวลารวมคือเวลาแปลงเป็น CNF บวกเวลาแก้ คำตอบที่ไม่เชื่อมต่อกันจะถูกหักล้างเมื่อพบเท่านั้น (lazy) และการหักล้างแต่ละครั้งต้องเรียก SAT เพิ่มอีกหนึ่งครั้ง
ยังไม่มีการแข่ง 待機中