Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Dynamic Symmetry Breaking in SAT Using Augmented Clauses with A Polynomial-time Lexicographic Pruning
Year (A.D.)
2018
Document Type
Thesis
First Advisor
อรรถสิทธิ์ สุรฤกษ์
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิศวกรรมศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2018.1248
Abstract
การเพิ่มความเร็วในการแก้ปัญหาความสอดคล้องแบบบูลนั้นสามารถทำได้ด้วยการใช้สมบัติของความสมมาตร หนึ่งในเทคนิคที่ใช้ประโยชน์จากความสมมาตรคือการหักล้างความสมมาตรพลวัต ซึ่งโดยปกติแล้วจะทำโดยการเพิ่มประพจน์เลือกที่สมมาตรกับประพจน์เลือกที่ถูกเรียนรู้ลงไปในนิพจน์บูลีนด้วย วิทยานิพนธ์ฉบับนี้จัดทำขึ้นเพื่อทำให้เทคนิคการหักล้างความสมมาตรพลวัตสามารถหักล้างความสมมาตรได้เป็นจำนวนที่เป็นเอกซ์โพเนนเชียลฟังก์ชันและใช้พื้นที่หน่วยความจำเป็นฟังก์ชันพหุนามของข้อมูลนำเข้า โดยใช้แนวคิดของประพจน์เลือกต่อเติมในกรณีที่กลุ่มความสมมาตรประกอบด้วยความสมมาตรแบบแถว วิทยานิพนธ์ฉบับนี้จะแสดงให้เห็นว่าปัญหาตัวขนย้ายลำดับที่เคซึ่งจำเป็นสำหรับการเผยแพร่ประพจน์เลือกเดี่ยวสามารถแก้ได้ในเวลาที่เป็นฟังก์ชันพหุนามเมื่อกลุ่มความสมมาตรเป็นความสมมาตรแบบแถว ผู้จัดทำยังได้ทำการศึกษาสมบัติของกลุ่มความสมมาตรที่มีความสมมาตรแบบแถวเป็นกลุ่มย่อยปกติ เช่น การแยกตัวประกอบเป็นผลคูณของความสมมาตรแบบแถวที่เป็นกลุ่มย่อยปกติ และความเป็นเอกลักษณ์ของการแยกตัวประกอบ เนื่องด้วยสมบัติเหล่านี้ ทางผู้จัดทำจึงได้เสนอวิธีการสร้างกลุ่มย่อยที่สามารถหาผลเฉลยได้ และเทคนิคการเล็มต้นไม้ค้นหาที่สมบูรณ์และสามารถทำได้ในเวลาที่เป็นฟังก์ชันพหุนามสำหรับปัญหาตัวขนย้ายลำดับที่เคภายใต้กลุ่มย่อยที่เราได้เสนอ และในส่วนสุดท้าย ผู้จัดทำได้ทำการวิเคราะห์บางแง่มุมของการการใช้งานเทคนิคที่ได้นำเสนอในวิทยานิพนธ์ฉบับนี้
Other Abstract (Other language abstract of ETD)
Symmetries in Boolean satisfiability problems (SAT) can be used for speeding-up solving the problems. One of the techniques that makes use of them is dynamic symmetry breaking. This technique often operates by adding symmetric versions of the learned clauses into the clause database. This thesis aims to achieve the coverage of exponentially many symmetries while using only polynomial size of space. To acquire our goal, we used the notion of augmented clauses in the cases of symmetry groups that contain a row symmetry group. We showed in this research that under the row symmetry groups, the search problems necessary for performing unit propagation could be solved in polynomial-time. Such a problem is called the k-transporters problems. We also explored some properties of the groups that contains row symmetry groups as normal subgroups. These properties include the factorizations of the group into products of row symmetry normal subgroup and the uniqueness of this factorization. Taking advantages of these properties we introduced the construction of solvable subgroups. And then, we devised a complete lexicographic pruning technique for the k-transporter problems that could be done in polynomial-time under our constructed subgroup. Lastly, we discussed some aspect of the implementation and some of its implications.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
ตรีธัญญพงศ์, เตวิช, "การหักล้างความสมมาตรพลวัตในปัญหาความสอดคล้องแบบบูลโดยใช้ประพจน์เลือกต่อเติมพร้อมด้วยการเล็มต้นไม้ค้นหาในเวลาเชิงพหุนาม" (2018). Chulalongkorn University Theses and Dissertations (Chula ETD). 3379.
https://digital.car.chula.ac.th/chulaetd/3379