การหักล้างความสมมาตรพลวัตในปัญหาความสอดคล้องแบบบูลโดยใช้ประพจน์เลือกต่อเติมพร้อมด้วยการเล็มต้นไม้ค้นหาในเวลาเชิงพหุนาม

Dynamic Symmetry Breaking in SAT Using Augmented Clauses with A Polynomial-time Lexicographic Pruning

Name: เตวิช ตรีธัญญพงศ์

Abstract: การเพิ่มความเร็วในการแก้ปัญหาความสอดคล้องแบบบูลนั้นสามารถทำได้ด้วยการใช้สมบัติของความสมมาตร หนึ่งในเทคนิคที่ใช้ประโยชน์จากความสมมาตรคือการหักล้างความสมมาตรพลวัต ซึ่งโดยปกติแล้วจะทำโดยการเพิ่มประพจน์เลือกที่สมมาตรกับประพจน์เลือกที่ถูกเรียนรู้ลงไปในนิพจน์บูลีนด้วย วิทยานิพนธ์ฉบับนี้จัดทำขึ้นเพื่อทำให้เทคนิคการหักล้างความสมมาตรพลวัตสามารถหักล้างความสมมาตรได้เป็นจำนวนที่เป็นเอกซ์โพเนนเชียลฟังก์ชันและใช้พื้นที่หน่วยความจำเป็นฟังก์ชันพหุนามของข้อมูลนำเข้า โดยใช้แนวคิดของประพจน์เลือกต่อเติมในกรณีที่กลุ่มความสมมาตรประกอบด้วยความสมมาตรแบบแถว วิทยานิพนธ์ฉบับนี้จะแสดงให้เห็นว่าปัญหาตัวขนย้ายลำดับที่เคซึ่งจำเป็นสำหรับการเผยแพร่ประพจน์เลือกเดี่ยวสามารถแก้ได้ในเวลาที่เป็นฟังก์ชันพหุนามเมื่อกลุ่มความสมมาตรเป็นความสมมาตรแบบแถว ผู้จัดทำยังได้ทำการศึกษาสมบัติของกลุ่มความสมมาตรที่มีความสมมาตรแบบแถวเป็นกลุ่มย่อยปกติ เช่น การแยกตัวประกอบเป็นผลคูณของความสมมาตรแบบแถวที่เป็นกลุ่มย่อยปกติ และความเป็นเอกลักษณ์ของการแยกตัวประกอบ เนื่องด้วยสมบัติเหล่านี้ ทางผู้จัดทำจึงได้เสนอวิธีการสร้างกลุ่มย่อยที่สามารถหาผลเฉลยได้ และเทคนิคการเล็มต้นไม้ค้นหาที่สมบูรณ์และสามารถทำได้ในเวลาที่เป็นฟังก์ชันพหุนามสำหรับปัญหาตัวขนย้ายลำดับที่เคภายใต้กลุ่มย่อยที่เราได้เสนอ และในส่วนสุดท้าย ผู้จัดทำได้ทำการวิเคราะห์บางแง่มุมของการการใช้งานเทคนิคที่ได้นำเสนอในวิทยานิพนธ์ฉบับนี้

Abstract: 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.

จุฬาลงกรณ์มหาวิทยาลัย. สำนักงานวิทยทรัพยากร

Address: กรุงเทพมหานคร

Email: cuir@car.chula.ac.th

Name: อรรถสิทธิ์ สุรฤกษ์

Role: ที่ปรึกษา

Created: 2561

Modified: 2563-08-09

Issued: 2563-08-09

วิทยานิพนธ์/Thesis

application/pdf

URL: http://cuir.car.chula.ac.th/handle/123456789/63656

tha

DegreeName: วิศวกรรมศาสตรมหาบัณฑิต

Level: ปริญญาโท

Descipline: วิศวกรรมคอมพิวเตอร์

Grantor: จุฬาลงกรณ์มหาวิทยาลัย

©copyrights จุฬาลงกรณ์มหาวิทยาลัย

ลำดับที่.	ชื่อแฟ้มข้อมูล	ขนาดแฟ้มข้อมูล	จำนวนเข้าถึง	วัน-เวลาเข้าถึงล่าสุด
1	6070194221.pdf	1.12 MB	2	2022-09-04 13:34:48

ใช้เวลา

0.028916 วินาที