ผลต่างระหว่างรุ่นของ "ทฤษฎีบทสี่สี"

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