Ioi16/test gen sat

input

input ของโปรแกรมในโจทย์ข้อ sat (ควรเป็น output ของคุณ) มีรูปแบบดังนี้

• บรรทัดแรกระบุ N และ M โดย N แทนจำนวนตัวแปร และ M แทนจำนวน clause (N <= 16, M <= 500) เรียกตัวแปรเป็น X1, X2,..., XN
• อีก M บรรทัดระบุข้อมูลของแต่ละ clause โดยแต่ละบรรทัดมีรูปแบบดังนี้
  • L V1 V2 ... VL โดยที่ L แทนจำนวนตัวแปรใน clause นั้น (L <= 5) และ V1 ... VL แทนหมายเลขตัวแปร ถ้าเป็นจำนวนเต็มบวก แสดงว่าใน clause เป็น XVi ถ้าเป็นเลขลบแสดงว่าใน clause เป็น not XVi

ตัวอย่าง

สมมติ เรามี CNF เป็น (x1 v x2 v ~x3) ^ (~x1 v x4 v x5) ^ (~x2 v ~x5) ข้อมูลป้อนเข้าจะเป็น

5 3
3 1 2 -3
3 -1 4 5
2 -2 -5

output

แต่ละโปรแกรมของ sat จะพิมพ์ผลลัพธ์รวม N บรรทัด เป็นค่าความจริงของตัวแปร X1, X2,..., XN ตามลำดับ โดยถ้าพิมพ์ 1 แสดงว่าเป็น true และ 0 จะเป็น false คะแนนที่ได้ของโปรแกรมสำหรับข้อมูลชุดนั้นจะเท่ากับจำนวน clause ที่เป็นจริงภายใต้ค่าความจริงดังกล่าว

โปรแกรมทดสอบ

ดาวน์โหลดได้ที่ http://theory.cpe.ku.ac.th/~jittat/ioi/2016/test-gen/sat/

• random - ตอบแบบสุ่ม
• randombest - สุ่มคำตอบไปเรื่อย ๆ จำนวน 1000 ครั้ง ตอบคำตอบที่ดีที่สุด
• randomwalk - สุ่มคำตอบ สุ่ม clause ที่ไม่จริง ปรับค่าตัวแปรบางตัวใน clause ให้ clause นั้นจริง ทำไปเรื่อย ๆ จำนวน 10,000 รอบ
• opt - ลองทุกแบบตอบคำตอบที่ดีที่สุด

โปรแกรมอื่น ๆ

• ev - โปรแกรมคำนวณจำนวน clause ที่คำตอบทำให้เป็นจริงได้ สั่งโดย ev input output