การใช้เหตุผลอัตโนมัติ: เครือข่ายมหาวิทยาลัย

รายละเอียด

ในหลักสูตรนี้คุณจะได้เรียนรู้วิธีการใช้เครื่องมือความพึงพอใจ (SAT / SMT) เพื่อแก้ไขปัญหาที่หลากหลาย
มีการให้ตัวอย่างพื้นฐานหลายอย่างเพื่อให้ได้รสชาติของแอพพลิเคชั่น: รูปสี่เหลี่ยมที่เหมาะสมที่จะใช้สำหรับการพิมพ์โปสเตอร์ปัญหาการตั้งเวลาการไขปริศนาและความถูกต้องของโปรแกรม นอกจากนี้ยังมีการนำเสนอทฤษฎีพื้นฐาน: การแก้ปัญหาเป็นวิธีพื้นฐานสำหรับความน่าพอใจเชิงประพจน์, กรอบการทำงานของ CDCL เพื่อขยายขนาดสำหรับสูตรขนาดใหญ่และวิธีการที่ง่ายต่อการจัดการกับความไม่เท่าเทียมเชิงเส้น

แนวทางที่เน้นน้ำหนักเบาในการทำตามหลักสูตรนี้คือเพียงแค่ดูการบรรยายและทำแบบทดสอบ เพื่อให้ได้รสชาติของหัวข้อนี้อาจได้ผลดี อย่างไรก็ตามแนวทางที่น่าสนใจกว่านั้นคือการใช้สิ่งนี้เป็นพื้นฐานในการประยุกต์ใช้ SAT / SMT กับปัญหาต่างๆเช่นปัญหาที่นำเสนอในงานที่ได้รับมอบหมายของเกียรติยศ