ผลต่างระหว่างรุ่นของ "ทฤษฎีบทสี่สี"
เนื้อหาที่ลบ เนื้อหาที่เพิ่ม
เพิ่มประวัติ+แก้ไขตอนเริ่มต้นเล็กน้อย |
ไม่มีความย่อการแก้ไข |
||
บรรทัด 35:
ในปี[[พ.ศ.2547]] [[เบนจามิน เวอร์เนอร์]](Benjamin Werner) และ [[จอร์จส์ กอนทิเออร์]](Georges Gonthier) พิสูจน์ทฤษฎีบทนี้ด้วยใช้โปรแกรมพิสูจน์ทฤษฎีบทชื่อ [[Coq]] ซึ่งช่วยลดความจำเป็นที่จะต้องเชื่อในความถูกต้องของโปรแกรมหลายๆโปรแกรม ที่ใช้ในการสอบกรณีแต่ละกรณี — เหลือเพียงแค่ต้องเชื่อใน Coq เท่านั้น
ตั้งแต่ได้มีการพิสูจน์ทฤษฎีบทนี้สำเร็จ อัลกอริทึมที่มีประสิทธิภาพมากมายก็ได้ถูกสร้างขึ้นสำหรับระบายสีแผนที่ด้วนสี่สี โดยทำงานในเวลาเพียง O(''n''<sup>2</sup>) เมื่อ ''n'' คือจำนวนจุดยอด นอกจากนี้ยังมีอัลกอริทึมทรงประสิทธิภาพที่สามารถตรวจสอบได้ว่าแผนที่ใช้สี 1 หรือ 2 สีระบายได้หรือไม่ สำหรับกรณี 3 สีนั้นเป็นปัญหา[[เอ็นพี
==รูปอย่างเป็นทางการในทฤษฎีกราฟ==
|