ในคณิตศาสตร์และวิทยาศาสตร์คอมพิวเตอร์ปัญหาการตัดสินใจ ( Entscheidungsproblem หรือ 'decision problem' ในภาษาเยอรมันออกเสียงว่า[ɛntˈʃaɪ̯dʊŋspʁoˌbleːm] ) เป็นความท้าทายที่David HilbertและWilhelm Ackermann ตั้งขึ้น ในปี 1928 ^{[ 1 ]}ปัญหานี้ต้องการอัลกอริทึมที่พิจารณาข้อความที่ป้อนเข้ามาและตอบว่า "ใช่" หรือ "ไม่ใช่" ตามความถูกต้องสากล กล่าวคือ ถูกต้องในทุกโครงสร้างอัลกอริทึมดังกล่าวได้รับการพิสูจน์แล้วว่าเป็นไปไม่ได้โดยAlonzo ChurchและAlan Turingในปี 1936

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

ในปี พ.ศ. 2479 Alonzo ChurchและAlan Turingได้ตีพิมพ์เอกสารอิสระ^{[ 2 ]}ซึ่งแสดงให้เห็นว่าวิธีแก้ปัญหาทั่วไปของEntscheidungsproblemนั้นเป็นไปไม่ได้ โดยถือว่าแนวคิดเชิงสัญชาตญาณของ " สามารถคำนวณได้อย่างมีประสิทธิภาพ " นั้นถูกจับโดยฟังก์ชันที่คำนวณได้โดยเครื่องจักร Turing (หรือเทียบเท่ากับฟังก์ชันที่แสดงได้ในแคลคูลัสแลมบ์ดา ) สมมติฐานนี้ปัจจุบันเรียกว่าวิทยานิพนธ์ Church– Turing

ที่มาของปัญหาEntscheidungsproblemย้อนกลับไปถึงGottfried Leibnizซึ่งในศตวรรษที่สิบเจ็ด หลังจากสร้างเครื่องคำนวณ เชิงกลที่ประสบความสำเร็จแล้ว เขาก็ฝันถึงการสร้างเครื่องจักรที่สามารถจัดการสัญลักษณ์เพื่อกำหนดค่าความจริงของข้อความทางคณิตศาสตร์^{[ 3 ]}เขาตระหนักว่าขั้นตอนแรกจะต้องเป็นภาษาทางการ ที่ชัดเจน และงานส่วนใหญ่ของเขาในเวลาต่อมามุ่งไปสู่เป้าหมายนั้น ในปี พ.ศ. 2461 David HilbertและWilhelm Ackermannได้ตั้งคำถามในรูปแบบที่ระบุไว้ข้างต้น

เพื่อสานต่อ "โครงการ" ของเขา ฮิลเบิร์ตได้ตั้งคำถามสามข้อในการประชุมนานาชาติในปี พ.ศ. 2461 โดยคำถามข้อที่สามกลายเป็นที่รู้จักในชื่อ " ปัญหาการตัดสินใจ ของฮิลเบิร์ต " ^{[ 4 ]}ในปี พ.ศ. 2462 โมเสส เชินฟิงเคิล ได้ตีพิมพ์บทความหนึ่งฉบับเกี่ยวกับกรณีพิเศษของปัญหาการตัดสินใจ ซึ่งจัดทำโดยพอล เบอร์เนย์ส^{[ 5 ]}

แม้กระทั่งในปี พ.ศ. 2473 ฮิลเบิร์ตก็ยังเชื่อว่าจะไม่มีปัญหาใดที่แก้ไม่ได้^{[ 6 ]}

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

คำตอบเชิงลบสำหรับปัญหาEntscheidungsproblemได้รับการเสนอโดย Alonzo Church ในปี 1935–36 ( ทฤษฎีบทของ Church ) และโดยอิสระในเวลาต่อมาไม่นานโดย Alan Turing ในปี 1936 ( การพิสูจน์ของ Turing ) Church พิสูจน์ว่าไม่มีฟังก์ชันที่คำนวณได้ใดๆ ที่สามารถตัดสินได้ว่านิพจน์ λ-calculus สองนิพจน์ที่กำหนดให้เทียบเท่ากันหรือไม่ เขาอาศัยงานก่อนหน้านี้ของStephen Kleene เป็นอย่างมาก Turing ลดคำถามเกี่ยวกับการมีอยู่ของ 'อัลกอริทึม' หรือ 'วิธีการทั่วไป' ที่สามารถแก้ปัญหา Entscheidungsproblem ได้เหลือเพียงคำถามเกี่ยวกับการมีอยู่ของ 'วิธีการทั่วไป' ที่ตัดสินได้ว่าเครื่องจักร Turing ใด ๆ หยุดทำงานหรือไม่ ( ปัญหาการหยุดทำงาน ) หากเข้าใจคำว่า 'อัลกอริทึม' ว่าหมายถึงวิธีการที่สามารถแสดงได้ด้วยเครื่องจักรทัวริง และคำตอบของคำถามหลังเป็นลบ (โดยทั่วไป) คำถามเกี่ยวกับการมีอยู่ของอัลกอริทึมสำหรับปัญหาการตัดสินใจก็ต้องเป็นลบ (โดยทั่วไป) เช่นกัน ในบทความปี 1936 ทัวริงกล่าวว่า: "สำหรับเครื่องคำนวณแต่ละเครื่อง 'it' เราสร้างสูตร 'Un(it)' และเราแสดงให้เห็นว่า หากมีวิธีการทั่วไปในการตรวจสอบว่า 'Un(it)' สามารถพิสูจน์ได้หรือไม่ ก็จะมีวิธีการทั่วไปในการตรวจสอบว่า 'it' เคยพิมพ์ 0 หรือไม่"

งานของทั้งเชิร์ชและทิวริงได้รับอิทธิพลอย่างมากจากงานก่อนหน้าของเคิร์ท เกอเดล เกี่ยวกับ ทฤษฎีบทความไม่สมบูรณ์โดยเฉพาะอย่างยิ่งวิธีการกำหนดหมายเลข ( การกำหนด หมายเลขแบบเกอเดล ) ให้กับสูตรตรรกะเพื่อลดทอนตรรกะให้เหลือเพียงเลขคณิต

ปัญหาEntscheidungsproblemเกี่ยวข้องกับปัญหาที่สิบของฮิลเบิร์ตซึ่งถามถึงอัลกอริทึมในการตัดสินว่าสมการไดโอแฟนไทน์มีคำตอบหรือไม่ การที่ไม่มีอัลกอริทึมดังกล่าว ซึ่งได้รับการพิสูจน์โดยงานของยูริ มาติยาเซวิชจูเลีย โรบินสันมาร์ติน เดวิสและฮิลารี พัตนัมโดยส่วนสุดท้ายของการพิสูจน์ในปี 1970 ก็หมายความว่าคำตอบของปัญหาEntscheidungsproblemคือ คำตอบเชิงลบเช่นกัน

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

โดยค่าเริ่มต้น การอ้างอิงในส่วนนี้มาจาก Pratt-Hartmann (2023) ^{[ 7 ]}

ปัญหา Entscheidungsproblemแบบคลาสสิกถามว่าสูตรลำดับที่หนึ่งเป็นจริงในทุกแบบจำลองหรือไม่ ปัญหาจำกัดถามว่าสูตรนั้นเป็นจริงในทุกแบบจำลองจำกัดหรือไม่ทฤษฎีบทของ Trakhtenbrotแสดงให้เห็นว่าปัญหานี้ก็ไม่สามารถตัดสินได้เช่นกัน^{[ 8 ] [ 7 ]}

สัญลักษณ์บางอย่าง: หมายถึงปัญหาในการตัดสินใจว่ามีแบบจำลองสำหรับชุดของสูตรตรรกะหรือไม่คือปัญหาเดียวกัน แต่สำหรับแบบจำลองจำกัดปัญหา - สำหรับส่วนย่อยตรรกะเรียกว่าสามารถตัดสินได้ หากมีโปรแกรมที่สามารถตัดสินได้สำหรับแต่ละชุดของสูตรตรรกะจำกัดในส่วนย่อยนั้น ว่ามีหรือไม่ ${\displaystyle {\rm {{วันเสาร์}(\พี )}}}$${\displaystyle \Phi }$${\displaystyle {\rm {{FinSat}(\พี )}}}$${\displaystyle {\rm {Sat}}}$${\displaystyle \Phi }$${\displaystyle {\rm {{วันเสาร์}(\พี )}}}$

มีการจัดลำดับชั้นของความสามารถในการตัดสินใจ โดยปัญหาที่ไม่สามารถตัดสินใจได้นั้นอยู่บนสุด และปัญหาที่สามารถตัดสินใจได้นั้นอยู่ถัดลงมา นอกจากนี้ ปัญหาที่สามารถตัดสินใจได้ยังสามารถแบ่งออกเป็นลำดับชั้นของความซับซ้อนได้อีกด้วย

ตรรกศาสตร์แบบอริสโตเติลพิจารณาประโยค 4 ประเภท ได้แก่ "p ทั้งหมดเป็น q", "p ทั้งหมดไม่ใช่ q", "p บางตัวเป็น q", และ "p บางตัวไม่ใช่ q" เราสามารถกำหนดรูปแบบของประโยคเหล่านี้ได้ในรูปของเศษส่วนของตรรกศาสตร์อันดับหนึ่ง โดยที่เป็นเพรดิเคตอะตอมิก และ. เมื่อกำหนดเซตจำกัดของสูตรตรรกศาสตร์แบบอริสโตเติลแล้วการตัดสิน ของ นั้น เป็นปัญหา NLOGSPACE สมบูรณ์ การตัดสิน ของ ก็เป็นปัญหา NLOGSPACE สมบูรณ์เช่นกันสำหรับการขยายเล็กน้อย (ทฤษฎีบท 2.7): ตรรกศาสตร์เชิงสัมพันธ์ขยายตรรกศาสตร์แบบอริสโตเติลโดยอนุญาตให้มีเพรดิเคตเชิงสัมพันธ์ ตัวอย่างเช่น "ทุกคนรักใครสักคน" สามารถเขียนได้เป็น. โดยทั่วไป เรามีประโยค 8 ประเภท: การตัดสิน ของ นั้นเป็น ปัญหา NLOGSPACE สมบูรณ์ (ทฤษฎีบท 2.15) ตรรกศาสตร์เชิงสัมพันธ์สามารถขยายไปสู่ประโยค 32 ประเภทได้โดยอนุญาตให้แต่การขยายนี้เป็นปัญหาEXPTIMEสมบูรณ์ (ทฤษฎีบท 2.24) $${\displaystyle \forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)}$$${\displaystyle p,q}$${\displaystyle +q:=q,\;-q:=\neg q}$${\displaystyle {\rm {Sat}}}$${\displaystyle {\rm {Sat}}}$$${\displaystyle \forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)}$$${\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}$$${\displaystyle {\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}}$$${\displaystyle {\rm {Sat}}}$${\displaystyle \pm p,\pm q}$

ส่วนย่อยตรรกะลำดับที่หนึ่งซึ่งมีชื่อตัวแปรเพียงอย่างเดียวคือNEXPTIME -complete (ทฤษฎีบท 3.18) เมื่อพิจารณาด้วยแล้วการตัดสินco-RE -complete และการตัดสินRE -complete (ทฤษฎีบท 3.15) จึงไม่สามารถตัดสินได้ ${\displaystyle x,y}$${\displaystyle x,y,z}$${\displaystyle {\rm {Sat}}}$${\displaystyle {\rm {FinSat}}}$

แคลคูลัสภาคแสดงเอกนาดิกคือแฟรกเมนต์ที่แต่ละสูตรประกอบด้วยภาคแสดงแบบ 1-ary เท่านั้น และไม่มีสัญลักษณ์ฟังก์ชัน แคลคูลัสนี้ สมบูรณ์แบบ NEXPTIME (ทฤษฎีบท 3.22) ${\displaystyle {\rm {Sat}}}$

สูตรลำดับที่หนึ่งใดๆ ก็มีรูปแบบปกติแบบพรีเน็กซ์ สำหรับคำนำหน้าตัวบ่งปริมาณที่เป็นไปได้แต่ละคำของรูปแบบปกติแบบพรีเน็กซ์ เราจะมีส่วนย่อยของตรรกะลำดับที่หนึ่ง ตัวอย่างเช่นคลาส Bernays–Schönfinkel , , คือคลาสของสูตรลำดับที่หนึ่งที่มีคำนำหน้าตัวบ่งปริมาณ, สัญลักษณ์ความเท่าเทียมและความสัมพันธ์ และไม่มีสัญลักษณ์ ฟังก์ชัน${\displaystyle [\exists ^{*}\forall ^{*}]_{=}}$${\displaystyle \exists \cdots \exists \forall \cdots \forall }$

ตัวอย่างเช่น บทความของทิวริงในปี 1936 (หน้า 263) สังเกตว่า เนื่องจากปัญหาการหยุดทำงานของเครื่องทิวริงแต่ละเครื่องเทียบเท่ากับสูตรตรรกะลำดับที่หนึ่งในรูปแบบ ดังนั้นปัญหาจึงไม่สามารถตัดสินได้ ${\displaystyle \forall \exists \forall \exists ^{6}}$${\displaystyle {\rm {{Sat}(\forall \exists \forall \exists ^{6})}}}$

ขอบเขตที่แน่นอนเป็นที่ทราบกันดีอยู่แล้ว:

• ${\displaystyle {\rm {{Sat}(\forall \exists \forall )}}}$และเป็นปัญหา co-RE-complete และปัญหาเหล่านั้นเป็นปัญหา RE-complete (ทฤษฎีบท 5.2)${\displaystyle {\rm {{Sat}([\forall \exists \forall ]_{=})}}}$${\displaystyle {\rm {FinSat}}}$
• เช่นเดียวกับ(ทฤษฎีบท 5.3)${\displaystyle \forall ^{3}\exists }$
• ${\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}$สามารถตัดสินได้ โดยได้รับการพิสูจน์อย่างอิสระโดย Gödel , SchütteและKalmár
• ${\displaystyle [\forall ^{2}\exists ]_{=}}$ไม่สามารถตัดสินได้
• สำหรับค่าใดๆทั้งและ ต่าง ก็เป็น NEXPTIME-complete (ทฤษฎีบท 5.1) ${\displaystyle n\geq 0}$${\displaystyle {\rm {{Sat}(\exists ^{n}\forall ^{*})}}}$${\displaystyle {\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}}$
  • สิ่งนี้หมายความว่าสามารถตัดสินได้ ซึ่งเป็นผลลัพธ์ที่ Bernays และ Schönfinkel เผยแพร่เป็นครั้งแรก^{[ 9 ]}${\displaystyle {\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}}$
• สำหรับค่าใดๆ ก็ตามจะถือว่าเสร็จสมบูรณ์ด้วย EXPTIME (ส่วนที่ 5.4.1)${\displaystyle n\geq 0,m\geq 2}$${\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}}$
• สำหรับค่าใดๆ ก็ตามจะถือว่าเสร็จสมบูรณ์ด้วย NEXPTIME (ส่วนที่ 5.4.2) ${\displaystyle n\geq 0}$${\displaystyle {\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}}$
  • สิ่งนี้หมายความว่าสามารถตัดสินได้ ซึ่งเป็นผลลัพธ์ที่ Ackermann เผยแพร่เป็นครั้งแรก^{[ 10 ]}${\displaystyle {\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}}$
• สำหรับค่าใดๆและค่าเหล่านั้นจะสมบูรณ์ตามมาตรฐาน PSPACE (ส่วนที่ 5.4.3)${\displaystyle n\geq 0}$${\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists )}}}$${\displaystyle {\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}}$

Börger et al. (2001) ^{[ 11 ]}อธิบายระดับความซับซ้อนในการคำนวณสำหรับเศษส่วนที่เป็นไปได้ทั้งหมดที่มีการรวมกันที่เป็นไปได้ทั้งหมดของคำนำหน้าตัวบ่งปริมาณ ฟังก์ชันอาร์ติซิตี้ พรีดิเคตอาร์ติซิตี้ และความเท่าเทียมกัน/ไม่เท่าเทียมกัน

การมีขั้นตอนการตัดสินใจที่เป็นรูปธรรมสำหรับสูตรตรรกะประเภทต่างๆ นั้นมีความสำคัญอย่างยิ่งสำหรับการตรวจสอบโปรแกรมและการตรวจสอบวงจร สูตรตรรกะบูลีนบริสุทธิ์มักจะถูกตัดสินโดยใช้ เทคนิค การแก้ปัญหา SATโดยอิงตาม อัลกอริธึ ม DPLL

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

• การพิสูจน์ทฤษฎีบทอัตโนมัติ
• ปัญหาข้อที่สองของฮิลเบิร์ต
• เครื่องออราเคิล
• การพิสูจน์ของทัวริง

• คำจำกัดความของentscheidungsproblemในพจนานุกรม Wiktionary