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

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

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/63656

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	อรรถสิทธิ์ สุรฤกษ์	-
dc.contributor.author	เตวิช ตรีธัญญพงศ์	-
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	-
dc.date.accessioned	2019-09-14T04:46:33Z	-
dc.date.available	2019-09-14T04:46:33Z	-
dc.date.issued	2561	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/63656	-
dc.description	วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561	-
dc.description.abstract	การเพิ่มความเร็วในการแก้ปัญหาความสอดคล้องแบบบูลนั้นสามารถทำได้ด้วยการใช้สมบัติของความสมมาตร หนึ่งในเทคนิคที่ใช้ประโยชน์จากความสมมาตรคือการหักล้างความสมมาตรพลวัต ซึ่งโดยปกติแล้วจะทำโดยการเพิ่มประพจน์เลือกที่สมมาตรกับประพจน์เลือกที่ถูกเรียนรู้ลงไปในนิพจน์บูลีนด้วย วิทยานิพนธ์ฉบับนี้จัดทำขึ้นเพื่อทำให้เทคนิคการหักล้างความสมมาตรพลวัตสามารถหักล้างความสมมาตรได้เป็นจำนวนที่เป็นเอกซ์โพเนนเชียลฟังก์ชันและใช้พื้นที่หน่วยความจำเป็นฟังก์ชันพหุนามของข้อมูลนำเข้า โดยใช้แนวคิดของประพจน์เลือกต่อเติมในกรณีที่กลุ่มความสมมาตรประกอบด้วยความสมมาตรแบบแถว วิทยานิพนธ์ฉบับนี้จะแสดงให้เห็นว่าปัญหาตัวขนย้ายลำดับที่เคซึ่งจำเป็นสำหรับการเผยแพร่ประพจน์เลือกเดี่ยวสามารถแก้ได้ในเวลาที่เป็นฟังก์ชันพหุนามเมื่อกลุ่มความสมมาตรเป็นความสมมาตรแบบแถว ผู้จัดทำยังได้ทำการศึกษาสมบัติของกลุ่มความสมมาตรที่มีความสมมาตรแบบแถวเป็นกลุ่มย่อยปกติ เช่น การแยกตัวประกอบเป็นผลคูณของความสมมาตรแบบแถวที่เป็นกลุ่มย่อยปกติ และความเป็นเอกลักษณ์ของการแยกตัวประกอบ เนื่องด้วยสมบัติเหล่านี้ ทางผู้จัดทำจึงได้เสนอวิธีการสร้างกลุ่มย่อยที่สามารถหาผลเฉลยได้ และเทคนิคการเล็มต้นไม้ค้นหาที่สมบูรณ์และสามารถทำได้ในเวลาที่เป็นฟังก์ชันพหุนามสำหรับปัญหาตัวขนย้ายลำดับที่เคภายใต้กลุ่มย่อยที่เราได้เสนอ และในส่วนสุดท้าย ผู้จัดทำได้ทำการวิเคราะห์บางแง่มุมของการการใช้งานเทคนิคที่ได้นำเสนอในวิทยานิพนธ์ฉบับนี้	-
dc.description.abstractalternative	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.	-
dc.language.iso	th	-
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.relation.uri	http://doi.org/10.58837/CHULA.THE.2018.1248	-
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.subject.classification	Computer Science	-
dc.title	การหักล้างความสมมาตรพลวัตในปัญหาความสอดคล้องแบบบูลโดยใช้ประพจน์เลือกต่อเติมพร้อมด้วยการเล็มต้นไม้ค้นหาในเวลาเชิงพหุนาม	-
dc.title.alternative	Dynamic Symmetry Breaking in SAT Using Augmented Clauses with A Polynomial-time Lexicographic Pruning	-
dc.type	Thesis	-
dc.degree.name	วิศวกรรมศาสตรมหาบัณฑิต	-
dc.degree.level	ปริญญาโท	-
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์	-
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.email.advisor	Athasit.S@Chula.ac.th	-
dc.identifier.DOI	10.58837/CHULA.THE.2018.1248	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
6070194221.pdf		1.15 MB	Adobe PDF	View/Open

Show simple item record