gophersat
1.0.0
นี่คือ Gophersat ซึ่งเป็นตัวแก้ปัญหา SAT และ pseudo-boolean ที่เขียนในภาษา Go ล้วนๆ Gophersat ได้รับการพัฒนาโดย CRIL (Centre de Recherche en Informatique de Lens) ที่ Artois University และ CNRS เผยแพร่ภายใต้ใบอนุญาต MIT Gophersat ค่อนข้างมีประสิทธิภาพ เช่น ในการวัดประสิทธิภาพ SAT ทั่วไป ระบบจะทำงานช้ากว่าโปรแกรมแก้ปัญหาระดับบนสุดประมาณ 2 ถึง 5 เท่า (เช่น กลูโคสหรือ minisat) ซึ่งเป็นแรงบันดาลใจอย่างมาก นอกจากนี้ยังสามารถแก้ปัญหา MAXSAT และปัญหาการตัดสินใจแบบบูลีนหลอกและการปรับให้เหมาะสมได้อีกด้วย
เวอร์ชันเสถียรล่าสุดของ Gophersat คือเวอร์ชัน 1.4 รวมถึงกลยุทธ์การแก้ปัญหาระนาบการตัดที่เป็นทางเลือก
ปัญหาบางอย่าง เช่น ปัญหาหลุมนกพิราบอันโด่งดัง ใช้เวลานานมากในการแก้ปัญหาโดยใช้การใช้เหตุผลเชิงตรรกะล้วนๆ
ปัญหาหลุมนกพิราบสามารถอธิบายได้ดังนี้: เป็นไปได้ไหมที่จะใส่นกพิราบ n ตัวลงใน m pigeonholes โดยที่ m = n-1 โดยไม่ต้องใส่นกพิราบหลายตัวลงในหลุมเดียวกันแล้วเอานกพิราบทั้งหมดไปไว้ในหลุม? คำตอบนั้นชัดเจน: หากคุณมีนกพิราบ 4 ตัวใน 3 หลุม คุณจะไม่สามารถวางนกพิราบทั้งหมดไว้ในหลุมอื่นได้ แต่คุณ จะพิสูจน์ สิ่งนี้ได้อย่างไร? นักแก้ปัญหา SAT หรือ PB จะพิสูจน์โดยลองใช้ชุดค่าผสมที่เป็นไปได้ทั้งหมด และจำนวนชุดค่าผสมที่เป็นไปได้จะเพิ่มขึ้นแบบทวีคูณ ดังนั้นการพยายามแก้ไขปัญหาด้วย n=20 จึงไม่สามารถทำได้ในทางปฏิบัติ แม้ว่าปัญหาจะมีคำตอบที่ชัดเจนก็ตาม
นักแก้ปัญหา PB บางรายใช้กลยุทธ์ทางเลือก: กลยุทธ์การตัดระนาบ จะไม่อธิบายโดยละเอียดในเอกสารนี้ แต่สถานะนี้สามารถมีประสิทธิภาพอย่างมากกับปัญหาบางอย่าง เช่น ปัญหานกพิราบซึ่งไม่สามารถแก้ไขได้อย่างมีประสิทธิภาพโดยใช้เหตุผลเชิงตรรกะล้วนๆ แต่จะช้ากว่าสำหรับปัญหาส่วนใหญ่
ขณะนี้สามารถใช้ระนาบการตัดกับ Gophersat ได้แล้ว เพียงใช้ตัวเลือกบรรทัดคำสั่ง -cp ดังนั้นแทนที่จะโทร:
gophersat problem.opb
เพียงโทร:
gophersat -cp problem.opb
เวอร์ชันเสถียรล่าสุดของ Gophersat คือเวอร์ชัน 1.3 เป็นการอัปเดตเล็กน้อย โดยเพิ่มความสามารถในการเข้าถึงตัวแก้ปัญหาพื้นฐานเมื่อจัดการกับปัญหา MAXSAT
Gophersat เวอร์ชัน 1.2 มีวิธีทำความเข้าใจอินสแตนซ์ UNSAT โดยให้ใบรับรอง RUP เมื่อปัญหาคือ UNSAT และโดยให้ความสามารถในการแยกชุดย่อยที่ไม่น่าพอใจของสูตร ข้อผิดพลาดในการแสดงผลได้รับการแก้ไขแล้ว และปรับปรุงการรองรับการแก้ไข SAT แบบค่อยเป็นค่อยไป
หากต้องการเรียนรู้เพิ่มเติมเกี่ยวกับฟังก์ชันเหล่านี้ คุณสามารถตรวจสอบบทช่วยสอนเกี่ยวกับใบรับรอง UNSAT และ MUS ได้
หากต้องการสร้างใบรับรองที่สามารถเรียกใช้งานได้ของ gophersat เพียงโทร:
gophersat -certified problem.cnf
จากนั้นใบรับรองจะถูกพิมพ์บนเอาต์พุตมาตรฐาน โดยใช้สัญลักษณ์ RUP ใบรับรองจะถูกสร้างขึ้นทันที ดังนั้นโปรดทราบว่าใบรับรองบางส่วนที่ไม่มีประโยชน์จะถูกสร้างขึ้น แม้ว่าปัญหาจะน่าพึงพอใจก็ตาม นี่เป็นวิธีปฏิบัติทั่วไปในชุมชน และแม้ว่าประโยคที่สร้างขึ้นจะไร้ประโยชน์ แต่ในทางปฏิบัติก็ไม่ใช่ปัญหา
หากต้องการแยก MUS ออกจากอินสแตนซ์ UNSAT เพียงโทร:
gophersat -mus problem.cnf
MUS จะถูกพิมพ์บนเอาต์พุตมาตรฐาน หากปัญหาไม่ใช่ UNSAT ข้อความแสดงข้อผิดพลาดจะปรากฏขึ้น
ในขณะนี้ สิ่งอำนวยความสะดวกเหล่านี้ใช้ได้เฉพาะกับปัญหา SAT ล้วนๆ เท่านั้น (เช่น ไม่ใช่ปัญหาหลอกบูลีน)
ตั้งแต่เวอร์ชัน 1.1 เป็นต้นมา Gophersat ได้รวมตัวแก้ปัญหาหลักใหม่ที่มีประสิทธิภาพมากขึ้นสำหรับปัญหา SAT ล้วนๆ และแพ็คเกจที่เกี่ยวข้องกับปัญหา MAXSAT นอกจากนี้ยังมี API ใหม่สำหรับการเพิ่มประสิทธิภาพและการนับโมเดล โดยที่โมเดลใหม่จะถูกเขียนลงในแชนเนลทันทีที่พบ
ตั้งแต่เวอร์ชัน 1.0 เป็นต้นมา API ของ Gophersat ถือว่าเสถียร ซึ่งหมายความว่า API จะรับประกันว่าจะเข้ากันได้แบบย้อนหลังจนกว่าจะมีการเปลี่ยนเวอร์ชันหลัก กล่าวอีกนัยหนึ่ง หากโปรแกรมของคุณทำงานกับ gophersat เวอร์ชัน 1.0 ก็จะยังคงใช้งานได้กับเวอร์ชัน 1.1 ขึ้นไป แต่ไม่จำเป็นต้องใช้กับเวอร์ชันที่สูงกว่า 2.0
โปรดทราบว่าโดย "ยังคงทำงานอยู่" เราหมายถึงเพียง "จะคอมไพล์และสร้างเอาต์พุตเดียวกัน" ไม่ใช่ "จะมีประสิทธิภาพด้านหน่วยความจำหรือด้านเวลาเท่ากัน" นี่คือข้อแตกต่างที่สำคัญ: ในระหว่างการอัพเกรดเวอร์ชันรอง ฮิวริสติกใหม่หรือประเภทข้อมูลสามารถเกิดขึ้นได้ ซึ่งหมายความว่าปัญหาบางอย่างอาจได้รับการแก้ไขเร็วขึ้นหรือช้าลงกว่าเดิม
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat สามารถใช้เป็นตัวแก้ปัญหาแบบสแตนด์อโลน (อ่านไฟล์ DIMACS CNF) หรือเป็นไลบรารีในโปรแกรม go ใดก็ได้
หากต้องการแก้ไขไฟล์ DIMACS คุณสามารถเรียก gophersat ด้วยไวยากรณ์ต่อไปนี้:
gophersat --verbose file.cnf
โดยที่ --verbose เป็นพารามิเตอร์ทางเลือกที่ทำให้ตัวแก้ปัญหาแสดงข้อมูลในระหว่างกระบวนการแก้ไข
Gophersat ยังสามารถอ่านและแก้ไขสูตรบูลีนทั่วไปได้ ไม่เพียงแต่ปัญหาที่แสดงในรูปแบบ DIMACS ที่ไม่เป็นมิตรต่อผู้ใช้เท่านั้น นอกจากนี้ยังเกี่ยวข้องกับข้อจำกัดเชิงจำนวนนับโดยธรรมชาติ กล่าวคือ ส่วนคำสั่งจะต้องมีค่าจริงอย่างน้อย n ตัวอักษร โดยมี n > 1
Gophersat สามารถใช้เป็นตัวแก้ปัญหาแบบสแตนด์อโลน (อ่านไฟล์ OPB) หรือเป็นไลบรารีในโปรแกรม go ใดก็ได้
ในการแก้ปัญหาหลอกบูลีน (ไม่ว่าจะเป็นการตัดสินใจหรือการเพิ่มประสิทธิภาพ) คุณสามารถเรียก gophersat ด้วยไวยากรณ์ต่อไปนี้:
gophersat --verbose file.opb
โดยที่ --verbose เป็นพารามิเตอร์ทางเลือกที่ทำให้ตัวแก้ปัญหาแสดงข้อมูลในระหว่างกระบวนการแก้ไข
ในขณะนี้ มันสามารถแก้ปัญหาที่เรียกว่า DEC-SMALLINT-LIN และ OPT-SMALLINT-LIN เท่านั้น เช่น ปัญหาการตัดสินใจ (มีวิธีแก้ไขหรือไม่) สำหรับข้อจำกัดเชิงเส้น (ผลรวมของตัวอักษรถ่วงน้ำหนัก) กับจำนวนเต็มเล็ก (n < 2^30) หรือปัญหาการหาค่าเหมาะที่สุด (วิธีแก้ไขที่ดีที่สุดคือการลดฟังก์ชันต้นทุนที่กำหนดให้เหลือน้อยที่สุด) สำหรับข้อจำกัดเชิงเส้นของจำนวนเต็มน้อย
ด้วยแพ็คเกจ maxsat ทำให้ Gophersat สามารถแก้ไขปัญหา MAXSAT ได้แล้ว
ในการแก้ปัญหา MAXSAT แบบถ่วงน้ำหนัก คุณสามารถเรียก gophersat ได้โดยใช้ไวยากรณ์ต่อไปนี้:
gophersat --verbose file.wcnf
โดยที่ --verbose เป็นพารามิเตอร์ทางเลือกที่ทำให้ตัวแก้ปัญหาแสดงข้อมูลในระหว่างกระบวนการแก้ไข ไฟล์ควรจะแสดงในรูปแบบ (รูปแบบ WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements]
SAT ซึ่งย่อมาจาก Boolean Satisfiability Problem เป็นปัญหา Canonical NP-complete กล่าวคือ ปัญหาที่ไม่มีวิธีแก้ปัญหาที่ทราบอยู่แล้วและไม่ได้ใช้เวลาเอ็กซ์โปเนนเชียลในกรณีที่แย่กว่านั้น กล่าวอีกนัยหนึ่ง นักแก้ปัญหา SAT พยายามค้นหาการมอบหมายสำหรับตัวแปรทั้งหมดที่ทำให้มันเป็นจริง สำหรับสูตรประพจน์ที่กำหนด หากมีการมอบหมายดังกล่าวอยู่
แม้ว่าการใช้โปรแกรมแก้ปัญหา SAT โดยใช้อัลกอริธึมแบบไร้เดียงสานั้นเป็นเรื่องเล็กน้อย แต่การใช้งานดังกล่าวจะไม่มีประสิทธิภาพมากนักในทางปฏิบัติ Gophersat ใช้คุณลักษณะที่ล้ำสมัยและค่อนข้างมีประสิทธิภาพ ทำให้สามารถใช้งานได้จริงในโปรแกรม Go ที่ต้องการกลไกการอนุมานที่มีประสิทธิภาพ
แม้ว่านี่จะไม่ใช่การตัดสินใจที่ดีที่สุดเสมอไปด้วยเหตุผลเชิงปฏิบัติ แต่ปัญหา NP-complete ใดๆ ก็สามารถแปลเป็นปัญหา SAT และแก้ไขได้โดย Gophersat ปัญหาดังกล่าว ได้แก่ ปัญหาพนักงานขายที่กำลังเดินทาง โปรแกรมจำกัด ปัญหากระเป๋าเป้สะพายหลัง การวางแผน การตรวจสอบแบบจำลอง การตรวจสอบความถูกต้องของซอฟต์แวร์ เป็นต้น
ข้อมูลเพิ่มเติมเกี่ยวกับปัญหา SAT สามารถพบได้ในบทความของวิกิพีเดียเกี่ยวกับ SAT
คุณยังสามารถค้นหาข้อมูลเกี่ยวกับวิธีแสดงสูตรบูลีนของคุณเองเพื่อให้ gophersat นำไปใช้ได้ในบทช่วยสอน "SAT สำหรับ noobs"
MAXSAT เป็นการเพิ่มประสิทธิภาพเทียบเท่ากับปัญหาการตัดสินใจของ SAT ในขณะที่โปรแกรมแก้ปัญหา SAT บริสุทธิ์จะส่งกลับแบบจำลองที่ตรงตามเงื่อนไขข้อคำสั่งทั้งหมดหรือ UNSAT หากไม่มีแบบจำลองดังกล่าวอยู่ โปรแกรมแก้ปัญหา MAXSAT จะส่งกลับแบบจำลองที่ตรงตามเงื่อนไขข้อคำสั่งต่างๆ มากที่สุดเท่าที่จะเป็นไปได้
มีส่วนขยายเป็น MAXSAT
MAXSAT บางส่วน หมายความว่า แม้ว่าเราต้องการตอบสนองอนุประโยคให้ได้มากที่สุดเท่าที่จะเป็นไปได้ แต่บางประโยค (เรียกว่า hard clauses ) ก็ต้อง ตอบสนองให้ได้ ไม่ว่าจะอย่างไรก็ตาม ปัญหา MAXSAT บางส่วนจึงสามารถประกาศได้ว่าไม่น่าพอใจ
ตัวอย่างเช่น การสร้างตารางเวลาสำหรับโรงเรียนเป็นปัญหา MAXSAT บางส่วน: มีทั้งแบบอ่อน (เช่น เราต้องการให้ชั้นเรียนน้อยที่สุดเท่าที่จะทำได้ โดยเริ่มหลัง 16.00 น. เป็นต้น) และแบบยาก (ครูสองคนไม่สามารถอยู่สองแห่งที่แตกต่างกันในเวลา ในเวลาเดียวกัน) ข้อจำกัด
MAXSAT แบบถ่วงน้ำหนัก หมายความว่าส่วนคำสั่งต่างๆ เชื่อมโยงกับต้นทุน: แม้ว่าจะเป็นทางเลือก แต่บางส่วนก็ถือว่ามีความสำคัญมากกว่าส่วนอื่นๆ ตัวอย่างเช่น ถ้าข้อ C1 มีราคา 3 และทั้งข้อ C2 และ C3 มีราคา 1 โซลูชันที่เป็นไปตาม C1 แต่ไม่มีทั้ง C2 และ C3 จะถือว่าดีกว่าโซลูชันที่ตรงตามความต้องการทั้ง C2 และ C3 แต่ไม่ใช่ C1 โซลูชันอื่นๆ ทั้งหมด สิ่งต่าง ๆ เท่าเทียมกัน
MAXSAT ที่ถ่วงน้ำหนักบางส่วน หมายความว่ามีทั้งอนุประโยคแบบอ่อนและแบบแข็งในปัญหา และมีการถ่วงน้ำหนักอนุประโยคแบบอ่อนด้วย ในเรื่องนี้ MAXSAT ที่ "บริสุทธิ์" เป็นกรณีเฉพาะของ MAXSAT ที่ถ่วงน้ำหนักบางส่วนทั่วไปมากกว่า: ปัญหา MAXSAT ที่ "บริสุทธิ์" คือปัญหา MAXSAT ที่ถ่วงน้ำหนักบางส่วน โดยที่อนุประโยคทั้งหมดเป็นอนุประโยคอ่อนที่เกี่ยวข้องกับน้ำหนักเท่ากับ 1
ปัญหา Pseudo-boolean ถือเป็นลักษณะทั่วไปของปัญหา SAT กล่าวคือ อนุประโยคเชิงประพจน์ใดๆ สามารถเขียนเป็นข้อจำกัดแบบ pseudo-boolean เดียวได้ แต่การแสดงข้อจำกัดแบบ pseudo-boolean อาจต้องใช้เลขยกกำลังของอนุประโยคเชิงประพจน์
นิพจน์หลอกบูลีน (เชิงเส้น) เป็นนิพจน์ดังนี้:
w1 l1 + w2 x2 + ... + wn xn ≥ y
โดยที่ y และ wi ทั้งหมดเป็นค่าคงที่จำนวนเต็ม และ li ทั้งหมดเป็นตัวอักษรบูลีน
เช่น เพื่อให้นิพจน์ต่อไปนี้เป็นจริง
2 ¬x1 + x2 + x3 ≥ 3
ตัวแปรบูลีน x1 ต้องเป็นเท็จ และอย่างน้อยหนึ่งใน x2 และ x3 จะต้องเป็นจริง นี่เทียบเท่ากับสูตรเชิงประพจน์
¬x1 ∧ (x2 ∨ x3)
นิพจน์หลอก-บูลีนเป็นลักษณะทั่วไปของอนุประโยคเชิงประพจน์: อนุประโยคใดๆ
x1 ∨ x2 ∨ ... ∨ xn
สามารถเขียนใหม่ได้เป็น
x1 + x2 + ... + xn ≥ 1
คำอธิบายของปัญหาหลอก-บูลีนอาจมีขนาดเล็กกว่าเชิงประพจน์เป็นเอกซ์โปเนนเชียล แต่การแก้ปัญหาบูลีนหลอกยังคงเป็น NP-สมบูรณ์
Gophersat แก้ปัญหาทั้งการตัดสินใจ (มีวิธีแก้ไขปัญหาหรือไม่) และปัญหาการปรับให้เหมาะสม ปัญหาการปรับให้เหมาะสมคือปัญหาบูลีนหลอกที่เกี่ยวข้องกับฟังก์ชันต้นทุน กล่าวคือ ผลรวมของเงื่อนไขที่ต้องย่อให้เล็กสุด แทนที่จะพยายามค้นหาแบบจำลองที่เป็นไปตามข้อจำกัดที่กำหนด gophersat จะพยายามค้นหาแบบจำลองที่รับประกันว่าจะเป็นไปตามข้อจำกัดและลดฟังก์ชันต้นทุนให้เหลือน้อยที่สุด
ในระหว่างการค้นหาโซลูชันที่เหมาะสมที่สุด gophersat จะจัดหาโซลูชันที่ต่ำกว่ามาตรฐาน (เช่น โซลูชันที่แก้ไขข้อจำกัดทั้งหมดแต่ยังไม่รับประกันว่าจะเหมาะสมที่สุด) ทันทีที่พบ ดังนั้นผู้ใช้สามารถรับโซลูชันที่ต่ำกว่ามาตรฐานในเวลาที่กำหนดได้ จำกัด หรือรออีกต่อไปเพื่อรับประกันวิธีแก้ปัญหาที่ดีที่สุด
ใช่และไม่ใช่ มันเร็วกว่าการใช้งานแบบไร้เดียงสามาก เร็วพอที่จะใช้กับปัญหาในโลกแห่งความเป็นจริง แต่ช้ากว่าโปรแกรมแก้ปัญหาระดับบนสุดที่ได้รับการปรับปรุงให้เหมาะสมที่สุดและล้ำสมัย
Gophersat ไม่ได้ตั้งเป้าที่จะเป็นนักแก้ปัญหา SAT/PB ที่เร็วที่สุดที่มีอยู่ เป้าหมายคือการให้การเข้าถึงเทคโนโลยี SAT และ PB แก่โกเฟอร์ โดยไม่ต้องใช้อินเทอร์เฟซกับนักแก้ปัญหาที่เขียนในภาษาอื่น (โดยทั่วไปคือ C/C++)
อย่างไรก็ตาม ในบางกรณี การเชื่อมต่อกับโปรแกรมแก้ปัญหาที่เขียนด้วยภาษาอื่นถือเป็นตัวเลือกที่ดีที่สุดสำหรับแอปพลิเคชันของคุณ หากคุณมีปัญหาเล็กๆ น้อยๆ มากมายที่ต้องแก้ไข Gophersat จะเป็นทางเลือกที่เร็วที่สุด สำหรับปัญหาที่ใหญ่กว่า หากคุณต้องการมีการพึ่งพาน้อยที่สุดเท่าที่จะเป็นไปได้โดยเสียเวลาในการแก้ปัญหา Gophersat ก็ดีเช่นกัน หากคุณต้องการแก้ไขปัญหายากๆ และไม่รังเกียจที่จะใช้ cgo หรือใช้โปรแกรมภายนอก Gophersat อาจไม่ใช่ตัวเลือกที่ดีที่สุด
มีนักแก้ปัญหา SAT อื่น ๆ สองสามคนใน Go ซึ่งส่วนใหญ่เป็น go-sat และ gini ประสิทธิภาพของ Gini ค่อนข้างเทียบเท่ากับ Gophersat แม้ว่าจะช้ากว่าเล็กน้อยโดยเฉลี่ยตามการทดสอบที่เราทำ
Gophersat ยังมอบฟีเจอร์เจ๋งๆ ที่ไม่มีให้ในโปรแกรมแก้ปัญหาอื่นๆ เสมอไป (เช่น รูปแบบอินพุตที่เป็นมิตรต่อผู้ใช้) ดังนั้นจึงสามารถใช้เป็นเครื่องมือในการอธิบายและแก้ไขปัญหา NP-hard ซึ่งสามารถลดเป็น SAT/PB ได้อย่างง่ายดาย ปัญหา.
ไม่ แพ็คเกจ bf (สำหรับ "สูตรบูลีน") อำนวยความสะดวกในการแปลสูตรบูลีนใดๆ เป็น CNF
สิ่งนี้เรียกว่าการนับแบบจำลอง และใช่ มีฟังก์ชันสำหรับสิ่งนั้น: solver.Solver.CountModels
คุณยังสามารถนับโมเดลจากบรรทัดคำสั่งได้ด้วย
gophersat --count filename
โดยที่ชื่อไฟล์อาจเป็นไฟล์ .opb หรือ .cnf
