ในตรรกศาสตร์และวิทยาศาสตร์คอมพิวเตอร์ปัญหาความสามารถในการทำให้เป็นจริงของบูลีน (บางครั้งเรียกว่าปัญหาความสามารถในการทำให้เป็นจริงของประพจน์และย่อว่าSATISFIABILITY , SATหรือB-SAT ) ถามว่ามีการตีความ ใด ที่ ทำให้ สูตรบูลีนที่กำหนดให้เป็นจริงหรือไม่ กล่าวอีกนัยหนึ่งคือ ถามว่าตัวแปรของสูตรสามารถแทนที่ด้วยค่า TRUE หรือ FALSE ได้อย่างสอดคล้องกันเพื่อให้สูตรมีค่าเป็น TRUE หรือไม่ ถ้าเป็นเช่นนั้น สูตรนั้นเรียกว่าสามารถทำให้เป็นจริงได้มิฉะนั้น เรียกว่า ไม่สามารถทำให้เป็นจริงได้ตัวอย่างเช่น สูตร " aและไม่ใช่b " สามารถทำให้เป็นจริงได้ เพราะสามารถหาค่าa = TRUE และb = FALSE ซึ่งทำให้ ( aและไม่ใช่b ) = TRUE ได้ ในทางตรงกันข้าม " aและไม่ใช่a " ไม่สามารถทำให้เป็นจริงได้

SAT เป็นปัญหาแรกที่ได้รับการพิสูจน์แล้วว่าเป็นNP-completeซึ่งก็คือทฤษฎีบท Cook–Levinหมายความว่าปัญหาทั้งหมดในกลุ่มความซับซ้อนNPซึ่งรวมถึงปัญหาการตัดสินใจและการเพิ่มประสิทธิภาพตามธรรมชาติที่หลากหลายนั้น มีความยากในการแก้ไขอย่างมากที่สุดเท่ากับ SAT ไม่มีอัลกอริทึมใดที่ทราบกันว่าสามารถแก้ปัญหา SAT แต่ละปัญหาได้อย่างมีประสิทธิภาพ (โดยที่ "มีประสิทธิภาพ" หมายถึง "กำหนดได้ในเวลาพหุนาม ") แม้ว่าโดยทั่วไปเชื่อกันว่าอัลกอริทึมดังกล่าวไม่มีอยู่จริง แต่ความเชื่อนี้ยังไม่ได้รับการพิสูจน์หรือหักล้างทางคณิตศาสตร์ การแก้ปัญหาว่า SAT มี อัลกอริทึม เวลาพหุนามหรือไม่ จะช่วยยุติปัญหา P เทียบกับ NPซึ่งเป็นหนึ่งในปัญหาเปิดที่สำคัญที่สุดในทฤษฎีการคำนวณ^{[ 1 ] [ 2 ]}

อย่างไรก็ตาม อัลกอริทึม SAT แบบฮิวริสติกสามารถแก้ปัญหาตัวอย่างที่เกี่ยวข้องกับตัวแปรหลายหมื่นตัวและสูตรที่ประกอบด้วยสัญลักษณ์นับล้าน^{[ 3 ]}ซึ่งเพียงพอสำหรับปัญหา SAT ในทางปฏิบัติหลายอย่างที่เกิดขึ้นในปัญญาประดิษฐ์การออกแบบวงจร [ ^{4 ]}และการ ^{พิสูจน์}ทฤษฎีบทอัตโนมัติ

สูตรตรรกะเชิงประพจน์หรือที่เรียกว่านิพจน์บูลีนสร้างขึ้นจากตัวแปร ตัวดำเนินการ AND ( การเชื่อม หรือแสดงด้วย ∧) OR ( การแยก ∨) NOT ( การปฏิเสธ ¬) และวงเล็บ สูตรจะเรียกว่าสามารถทำให้เป็นจริงได้หากสามารถทำให้เป็นจริงได้โดยการกำหนดค่าตรรกะ ที่เหมาะสม (เช่น จริง เท็จ) ให้กับตัวแปรปัญหาความสามารถในการทำให้เป็นจริงของบูลีน (SAT) คือการตรวจสอบว่าสูตรที่กำหนดนั้นสามารถทำให้เป็นจริงได้หรือไม่ปัญหาการตัดสินใจ นี้ มีความสำคัญอย่างยิ่งในหลายสาขาของ^{วิทยาศาสตร์}คอมพิวเตอร์รวมถึงวิทยาศาสตร์คอมพิวเตอร์เชิงทฤษฎีทฤษฎีความซับซ้อน^{[ 5 ] [ 6 ]}อัลกอริทึมศาสตร์การเข้ารหัส^{[ 7 ] [ 8 ]}และปัญญาประดิษฐ์ [ ^{9 ]}

ตัวแปร(literal)คือตัวแปร (ในกรณีนี้เรียกว่าตัวแปรบวก ) หรือค่าปฏิเสธของตัวแปร (เรียกว่าตัวแปรลบ ) อนุประโยค (clause)คือการเชื่อมกันของตัวแปร (หรือตัวแปรเดียว) อนุประโยคเรียกว่าอนุ ประโยค ฮอร์น (Horn clause ) ถ้ามีตัวแปรบวกอย่างมากที่สุดหนึ่งตัว สูตรอยู่ในรูปแบบปกติแบบเชื่อมประโยค (Conjunctive Normal Form : CNF) ถ้าเป็นการเชื่อมกันของอนุประโยค (หรืออนุประโยคเดียว)

ตัวอย่างเช่นx ₁เป็นตัวแปรเชิงบวก¬ x ₂เป็นตัวแปรเชิงลบ และx ₁ ∨ ¬ x ₂เป็นอนุประโยค สูตร( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁อยู่ในรูปประโยคปกติแบบเชื่อมโยง อนุประโยคแรกและอนุประโยคที่สามเป็นอนุประโยคฮอร์น แต่อนุประโยคที่สองไม่ใช่ สูตรนี้สามารถหาคำตอบได้ โดยการเลือกx ₁  = FALSE, x ₂  = FALSE และx ₃ตามอำเภอใจ เนื่องจาก (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x ₃ ) ∧ ¬FALSE จะมีค่าเป็น (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x ₃ ) ∧ TRUE และในทางกลับกันจะเป็น TRUE ∧ TRUE ∧ TRUE (กล่าวคือ TRUE) ในทางตรงกันข้าม สูตร CNF a ∧ ¬ aซึ่งประกอบด้วยข้อความสองข้อความที่มีตัวแปรเดียว ไม่สามารถหาคำตอบได้ เนื่องจากสำหรับa =TRUE หรือa =FALSE จะได้ผลลัพธ์เป็น TRUE ∧ ¬TRUE (นั่นคือ FALSE) หรือ FALSE ∧ ¬FALSE (นั่นคือ FALSE อีกครั้ง) ตามลำดับ

สำหรับปัญหา SAT บางเวอร์ชัน การกำหนดแนวคิดของ สูตร รูปแบบปกติแบบเชื่อมโยงทั่วไป (generalized conjunctive normal form formula) นั้นมีประโยชน์ กล่าวคือ เป็นการเชื่อมโยงของข้อความทั่วไป จำนวนมากโดยพลการ ซึ่งข้อความทั่วไปเหล่านี้มีรูปแบบR ( l ₁ ,..., l _n )สำหรับฟังก์ชันบูลีนRและตัวอักษร (ธรรมดา) l _iชุดฟังก์ชันบูลีนที่อนุญาตต่างกันจะนำไปสู่เวอร์ชันของปัญหาที่แตกต่างกัน ตัวอย่างเช่นR (¬ x , a , b ) เป็นข้อความทั่วไป และR (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) เป็นรูปแบบปกติแบบเชื่อมโยงทั่วไป สูตรนี้จะถูกใช้ด้านล่างโดยที่Rเป็นตัวดำเนินการไตรภาคที่เป็นจริงก็ต่อเมื่ออาร์กิวเมนต์ตัวใดตัวหนึ่งเป็นจริงเท่านั้น

โดยใช้กฎของพีชคณิตบูลีนสูตรตรรกะเชิงประพจน์ทุกสูตรสามารถแปลงเป็นรูปแบบปกติเชิงเชื่อมโยงที่เทียบเท่ากันได้ ซึ่งอาจมีความยาวเพิ่มขึ้นแบบเลขชี้กำลัง ตัวอย่างเช่น การแปลงสูตร ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) ให้เป็นรูปแบบปกติเชิงเชื่อมโยงจะได้

ในขณะที่แบบแรกเป็นการเชื่อมแบบ" หรือ" ของ การเชื่อมแบบ "หรือ" n ครั้งที่มีตัวแปร 2 ตัว แบบหลังประกอบด้วยประโยคย่อย 2n ^{ประโยค}ที่มีตัวแปร n ตัว

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

SAT เป็นปัญหาแรกที่ทราบว่าเป็นNP-completeดังที่พิสูจน์โดยStephen Cookที่มหาวิทยาลัยโทรอนโตในปี 1971 ^{[ 10 ]}และโดยLeonid Levinที่สถาบันวิทยาศาสตร์แห่งรัสเซียในปี 1973 ^{[ 11 ]}จนถึงเวลานั้น แนวคิดของปัญหา NP-complete ยังไม่มีอยู่จริง การพิสูจน์แสดงให้เห็นว่าปัญหาการตัดสินใจทุกปัญหาในระดับความซับซ้อนNPสามารถลดรูปเป็นปัญหา SAT สำหรับสูตร CNF ^{[ a ]} ​​ซึ่งบางครั้งเรียกว่า CNFSATคุณสมบัติที่มีประโยชน์ของการลดรูปของ Cook คือการรักษาจำนวนคำตอบที่ยอมรับได้ ตัวอย่างเช่น การตัดสินใจว่ากราฟ ที่กำหนด มี3 สีหรือไม่เป็นอีกปัญหาหนึ่งใน NP หากกราฟมี 3 สีที่ถูกต้อง 17 สี สูตร SAT ที่สร้างขึ้นโดยการลดรูปของ Cook–Levin จะมีการกำหนดค่าที่น่าพอใจ 17 รายการ

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

เช่นเดียวกับปัญหาความสามารถในการทำให้เป็นจริงสำหรับสูตรใดๆ การหาความสามารถในการทำให้เป็นจริงของสูตรในรูปแบบปกติแบบเชื่อมโยงซึ่งแต่ละประโยคย่อยจำกัดอยู่ที่ตัวอักษรไม่เกินสามตัวก็เป็นปัญหา NP-complete เช่นกัน ปัญหานี้เรียกว่า3-SAT , 3CNFSATหรือ3-satisfiabilityเพื่อลดปัญหา SAT ที่ไม่จำกัดให้เป็น 3-SAT ให้แปลงแต่ละประโยคย่อยl ₁ ∨ ⋯ ∨ l _nให้เป็นการเชื่อมโยงของ ประโยคย่อย n - 2ประโยค

โดยที่x ₂ , ⋯ , x _{n −2}เป็นตัวแปรใหม่ที่ไม่ปรากฏที่อื่น แม้ว่าสูตรทั้งสองจะไม่สมมูลกันทางตรรกะแต่ก็สามารถทำให้เป็นจริงได้เท่ากันสูตรที่ได้จากการแปลงข้อความทั้งหมดมีความยาวไม่เกิน 3 เท่าของสูตรเดิม นั่นคือ การเติบโตของความยาวเป็นแบบพหุนาม^{[ 12 ]}

3-SAT เป็นหนึ่งใน21 ปัญหา NP-complete ของ Karpและใช้เป็นจุดเริ่มต้นในการพิสูจน์ว่าปัญหาอื่นๆ ก็เป็นปัญหาNP-hardเช่น กัน ^{[ b ]}โดยใช้วิธีลดรูปพหุนามจาก 3-SAT ไปยังปัญหาอื่นๆ ตัวอย่างของปัญหาที่ใช้วิธีนี้คือปัญหาคลิก : กำหนดสูตร CNF ที่ประกอบด้วยc ข้อความ กราฟที่สอดคล้องกันจะมีจุดยอดสำหรับแต่ละตัวอักษร และขอบระหว่างตัวอักษรที่ไม่ขัดแย้งกันสองตัว^{[ c ]}จากข้อความที่ต่างกัน ดูภาพประกอบ กราฟจะมีc-คลิกก็ต่อเมื่อสูตรนั้นสามารถทำให้เป็นจริงได้^{[ 13 ]}

มีอัลกอริทึมแบบสุ่มอย่างง่ายจาก Schöning (1999) ที่ทำงานในเวลา (4/3) ⁿโดยที่nคือจำนวนตัวแปรในข้อเสนอ 3-SAT และประสบความสำเร็จด้วยความน่าจะเป็นสูงที่จะตัดสิน 3-SAT ได้อย่างถูกต้อง^{[ 14 ]}

สมมติฐานเวลาแบบเอกซ์โปเนนเชียลยืนยันว่าไม่มีอัลกอริทึมใดที่สามารถแก้ปัญหา 3-SAT (หรือk -SAT สำหรับk > 2 ใดๆ ) ได้ใน เวลา exp( o ( n )) (นั่นคือ เร็วกว่าแบบเอกซ์โปเนนเชียลในn อย่างมาก )

Selman, Mitchell และ Levesque (1996) ให้ข้อมูลเชิงประจักษ์เกี่ยวกับความยากของสูตร 3-SAT ที่สร้างขึ้นแบบสุ่ม โดยขึ้นอยู่กับพารามิเตอร์ขนาด ความยากวัดจากจำนวนการเรียกซ้ำที่ทำโดยอัลกอริทึม DPLLพวกเขาระบุพื้นที่การเปลี่ยนเฟสจากสูตรที่เกือบจะแน่นอนสามารถทำให้พอใจได้ไปสู่สูตรที่เกือบจะแน่นอนไม่สามารถทำให้พอใจได้ที่อัตราส่วนของข้อความต่อตัวแปรประมาณ 4.26 ^{[ 15 ]}

3-satisfiability สามารถขยายไปสู่​​k- satisfiability ( k -SATหรือk -CNF-SAT ) ได้ เมื่อพิจารณาสูตรใน CNF โดยแต่ละข้อความมีตัวอักษรได้ มากถึง k ตัว ^{[ 16 ]}อย่างไรก็ตาม เนื่องจากสำหรับk ≥ 3 ใดๆ ปัญหานี้จึงไม่สามารถง่ายกว่า 3-SAT หรือยากกว่า SAT ได้ และปัญหาทั้งสองหลังเป็น NP-complete ดังนั้นจึงต้องเป็นk -SAT

ผู้เขียนบางคนจำกัดk -SAT ไว้ที่สูตร CNF ที่มีตัวอักษรkตัวพอดีซึ่งไม่ได้นำไปสู่คลาสความซับซ้อนที่แตกต่างกันเช่นกัน เนื่องจากแต่ละข้อความที่มีตัวอักษรน้อยกว่าkตัวสามารถเติมด้วยสำเนาตัวอักษรเดียวกันซ้ำได้^{[ 17 ]}

ความสามารถในการตอบสนองและเรขาคณิตของพื้นที่คำตอบของ ปัญหา k -SAT ที่มีข้อความที่สร้างขึ้นแบบสุ่มได้รับการตรวจสอบทางสถิติแล้ว แบบจำลองนี้แสดงให้เห็นถึงการเปลี่ยนแปลงเฟสต่างๆ เกี่ยวกับความสามารถในการตอบสนองและเรขาคณิตของพื้นที่คำตอบ โดยขึ้นอยู่กับอัตราส่วนของข้อความต่อตัวแปร (หรือที่เรียกว่าความหนาแน่น) สำหรับความสามารถในการตอบสนองนั้น มีเกณฑ์ที่ชัดเจนอยู่ค่าหนึ่ง ซึ่งด้วยความน่าจะเป็นสูง คำตอบจะมีอยู่ก็ต่อเมื่อความหนาแน่นยังคงต่ำกว่าเกณฑ์นี้^{[ 18 ]}ต่ำกว่าเกณฑ์ความสามารถในการตอบสนองมาก พื้นที่คำตอบยังมีการเปลี่ยนแปลงเฟสทางเรขาคณิตอีกด้วย กล่าวคือ มันจะแตกออกเป็นกลุ่มที่แยกออกจากกันอย่างชัดเจนจำนวนมากแบบเลขชี้กำลัง การเริ่มต้นของการเปลี่ยนแปลงเฟสนี้ตรงกับเกณฑ์อัลกอริทึมที่ทราบ ซึ่งชี้ให้เห็นถึงความเชื่อมโยงระหว่างเรขาคณิตและความยากลำบากในการแก้ปัญหาด้วยอัลกอริทึม^{[ 19 ] [ 20 ]}

รูปแบบปกติของการเชื่อมโยง (โดยเฉพาะอย่างยิ่งที่มีตัวแปร 3 ตัวต่อประโยค) มักถูกพิจารณาว่าเป็นรูปแบบมาตรฐานสำหรับการแสดงสูตร SAT ดังที่แสดงไว้ข้างต้น ปัญหา SAT ทั่วไปจะลดลงเหลือ 3-SAT ซึ่งเป็นปัญหาของการพิจารณาความสามารถในการทำให้เป็นจริงสำหรับสูตรในรูปแบบนี้

สูตร 3-SAT เรียกว่าLinear SAT ( LSAT ) หากแต่ละข้อความ (ซึ่งมองว่าเป็นเซตของตัวอักษร) ตัดกับข้อความอื่นได้ไม่เกินหนึ่งข้อความ และยิ่งไปกว่านั้น หากข้อความสองข้อความตัดกัน พวกมันจะมีตัวอักษรที่เหมือนกันเพียงหนึ่งตัวเท่านั้น สูตร LSAT สามารถแสดงได้เป็นเซตของช่วงกึ่งปิดที่ไม่ทับซ้อนกันบนเส้นตรง การตัดสินว่าสูตร LSAT สามารถทำให้เป็นจริงได้หรือไม่นั้นเป็นปัญหา NP-complete ^{[ 21 ]}

ปัญหา SAT จะง่ายขึ้นหากจำนวนตัวแปรในประโยคจำกัดไว้ที่อย่างมาก 2 ตัว ซึ่งในกรณีนี้ ปัญหาจะเรียกว่า2-SATปัญหานี้สามารถแก้ไขได้ในเวลาพหุนาม และในความเป็นจริงแล้วเป็นปัญหาที่สมบูรณ์สำหรับระดับความซับซ้อนNLหากเปลี่ยนการดำเนินการ OR ทั้งหมดในตัวแปรเป็นการดำเนิน การ XORผลลัพธ์ที่ได้จะเรียกว่าexclusive-or 2-satisfiabilityซึ่งเป็นปัญหาที่สมบูรณ์สำหรับระดับความซับซ้อนSL = L

ปัญหาของการตัดสินความสามารถในการทำให้เป็นจริงของการเชื่อมโยงของข้อความ Horn ที่กำหนด เรียกว่าHorn-satisfiabilityหรือHORN-SATสามารถแก้ไขได้ในเวลาพหุนามด้วยขั้นตอนเดียวของ อัลกอริธึม การแพร่กระจายหน่วยซึ่งสร้างแบบจำลองขั้นต่ำเพียงแบบเดียวของชุดข้อความ Horn (โดยสัมพันธ์กับชุดของตัวอักษรที่กำหนดให้กับ TRUE) Horn-satisfiability เป็นปัญหาP-completeสามารถมองได้ว่าเป็น เวอร์ชัน Pของปัญหาความสามารถในการทำให้เป็นจริงแบบบูลีน นอกจากนี้ การตัดสินความจริงของสูตร Horn ที่มีปริมาณสามารถทำได้ในเวลาพหุนาม^{[ 22 ]}

ประโยคเงื่อนไขแบบฮอร์นมีความน่าสนใจเพราะสามารถแสดงถึงการบ่งชี้ของตัวแปรหนึ่งจากชุดของตัวแปรอื่น ๆ ได้ ตัวอย่างเช่น ประโยคเงื่อนไข ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ yสามารถเขียนใหม่ได้เป็นx ₁ ∧ ... ∧ x _n → yนั่นคือ ถ้าx ₁ ,..., x _nเป็นจริงทั้งหมดแล้วyก็ต้องเป็นจริงด้วย

การขยายความทั่วไปของกลุ่มสูตรฮอร์นคือกลุ่มสูตรฮอร์นที่เปลี่ยนชื่อได้ ซึ่งเป็นเซตของสูตรที่สามารถจัดให้อยู่ในรูปฮอร์นได้โดยการแทนที่ตัวแปรบางตัวด้วยนิเสธของตัวแปรนั้น ตัวอย่างเช่น ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ไม่ใช่สูตรฮอร์น แต่สามารถเปลี่ยนชื่อเป็นสูตรฮอร์น ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁โดยการนำy ₃ มา เป็นนิเสธของx ₃ในทางตรงกันข้าม การเปลี่ยนชื่อ ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ ไม่ นำไปสู่สูตรฮอร์น การตรวจสอบการมีอยู่ของการแทนที่ดังกล่าวสามารถทำได้ในเวลาเชิงเส้น ดังนั้น ความสามารถในการทำให้เป็นจริงของสูตรดังกล่าวจึงอยู่ใน P เนื่องจากสามารถแก้ไขได้โดยการดำเนินการแทนที่นี้ก่อน แล้วจึงตรวจสอบความสามารถในการทำให้เป็นจริงของสูตรฮอร์นที่ได้

ปัญหา SAT นั้นง่ายมากหากสูตรถูกจำกัดให้อยู่ในรูปแบบปกติแบบแยกส่วน (disjunctive normal form)กล่าวคือ เป็นการแยกส่วนของการเชื่อมโยงของตัวแปร สูตรดังกล่าวจะสามารถทำให้เป็นจริงได้ก็ต่อเมื่ออย่างน้อยหนึ่งในการเชื่อมโยงสามารถทำให้เป็นจริงได้ และการเชื่อมโยงสามารถทำให้เป็นจริงได้ก็ต่อเมื่อมันไม่มีทั้งxและ NOT xสำหรับตัวแปรx บางตัว สามารถตรวจสอบได้ในเวลาเชิงเส้น ยิ่งไปกว่านั้น หากจำกัดให้สูตรอยู่ในรูปแบบปกติแบบแยกส่วนที่สมบูรณ์ (full disjunctive normal form ) ซึ่งตัวแปรทุกตัวปรากฏเพียงครั้งเดียวในการเชื่อมโยงแต่ละครั้ง ก็สามารถตรวจสอบได้ในเวลาคงที่ (constant time) (การเชื่อมโยงแต่ละครั้งแสดงถึงการกำหนดค่าที่ทำให้เป็นจริงหนึ่งค่า) แต่การแปลงปัญหา SAT ทั่วไปให้เป็นรูปแบบปกติแบบแยกส่วนอาจใช้เวลาและพื้นที่แบบเลขชี้กำลัง ตัวอย่างเช่น ลองเปลี่ยน "∧" และ "∨" ในตัวอย่างการระเบิดแบบเลขชี้กำลัง ข้างต้น เป็นรูปแบบปกติแบบเชื่อมโยง (conjunctive normal forms)

อีกรูปแบบหนึ่งของปัญหา NP-complete ของปัญหา 3-satisfiability คือ3-SAT แบบหนึ่งในสาม (หรือที่รู้จักกันในชื่อ1-in-3-SATและexactly-1 3-SAT ) โดยกำหนดให้รูปแบบปกติแบบเชื่อมโยงที่มีตัวแปรสามตัวต่อประโยคย่อย ปัญหาคือการพิจารณาว่ามีการกำหนดค่าความจริงให้กับตัวแปรหรือไม่ เพื่อให้แต่ละประโยคย่อยมี ตัวแปรที่เป็นจริง เพียงหนึ่งตัว (และมีตัวแปรที่เป็นเท็จสองตัว)

อีกรูปแบบหนึ่งคือ ปัญหา ความพึงพอใจ 3 ประการที่ไม่เท่ากันทั้งหมด (เรียกอีกอย่างว่าNAE3SAT ) เมื่อกำหนดรูปแบบปกติแบบเชื่อมโยงที่มีตัวอักษรสามตัวต่อประโยค ปัญหาคือการพิจารณาว่ามีการกำหนดค่าให้กับตัวแปรหรือไม่ โดยที่ไม่มีประโยคใดที่ตัวอักษรทั้งสามตัวมีค่าความจริงเดียวกัน ปัญหานี้เป็นปัญหา NP-complete เช่นกัน แม้ว่าจะไม่มีสัญลักษณ์การปฏิเสธก็ตาม ตามทฤษฎีบทการแบ่งแยกของ Schaefer ^{[ 23 ]}

กรณีพิเศษอีกประการหนึ่งคือคลาสของปัญหาที่แต่ละข้อความประกอบด้วยตัวดำเนินการ XOR (เช่นเอกสิทธิ์เฉพาะหรือ ) แทนที่จะเป็นตัวดำเนินการ OR (ธรรมดา) ซึ่งอยู่ในPเนื่องจากสูตร XOR-SAT สามารถมองได้ว่าเป็นระบบสมการเชิงเส้น mod 2 และสามารถแก้ได้ในเวลาลูกบาศก์โดยการกำจัดแบบเกาส์เซียน^{[ 24 ]}

ข้อจำกัดข้างต้น (CNF, 2CNF, 3CNF, Horn, XOR-SAT) กำหนดให้สูตรที่พิจารณาต้องเป็นผลรวมของสูตรย่อย โดยแต่ละข้อจำกัดจะระบุรูปแบบเฉพาะสำหรับสูตรย่อยทั้งหมด เช่น ใน 2CNF เฉพาะประโยคไบนารีเท่านั้นที่สามารถเป็นสูตรย่อยได้

ทฤษฎีบทการแบ่งแยกของ Schaefer ระบุว่า สำหรับข้อจำกัดใดๆ ของฟังก์ชันบูลีนที่สามารถใช้สร้างสูตรย่อยเหล่านี้ได้ ปัญหาความพึงพอใจที่สอดคล้องกันจะอยู่ใน P หรือ NP-complete การเป็นสมาชิกใน P ของความพึงพอใจของสูตร 2CNF, Horn และ XOR-SAT เป็นกรณีพิเศษของทฤษฎีบทนี้^{[ 23 ]}

ตารางต่อไปนี้สรุปรูปแบบต่างๆ ของข้อสอบ SAT ที่พบได้ทั่วไป

ส่วนขยายที่ได้รับความนิยมอย่างมากตั้งแต่ปี 2003 คือsatisfiability modulo theories ( SMT ) ซึ่งสามารถเสริมสูตร CNF ด้วยข้อจำกัดเชิงเส้น อาร์เรย์ ข้อจำกัดที่แตกต่างกันทั้งหมดฟังก์ชันที่ไม่ได้ตีความ [ ^{25 ] เป็นต้น ส่วนขยายดังกล่าวโดย ทั่วไป}ยังคงเป็น NP-complete แต่ปัจจุบันมีตัวแก้ปัญหาที่มีประสิทธิภาพมากที่สามารถจัดการกับข้อจำกัดหลายประเภทดังกล่าวได้

ปัญหาความน่าพอใจจะซับซ้อนมากขึ้นหากอนุญาตให้ใช้ตัวบ่งปริมาณ ทั้ง "สำหรับทุก" ( ∀ ) และ "มีอยู่" ( ∃ ) ในการผูกตัวแปรบูลีน ตัวอย่างของนิพจน์ดังกล่าวคือ ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; ซึ่งถูกต้อง เนื่องจากสำหรับทุกค่าของxและyสามารถหาค่าz ที่เหมาะสมได้ กล่าวคือ z = TRUE ถ้าทั้งxและyเป็น FALSE และz = FALSE ในกรณีอื่น ๆ ทฤษฎีบทความน่าพอใจ (SAT) เอง (โดยปริยาย) ใช้เฉพาะตัวบ่งปริมาณ ∃ เท่านั้น หากอนุญาตให้ใช้เฉพาะตัวบ่งปริมาณ ∀ แทน จะได้ ปัญหา ที่เรียกว่าปัญหาสัจนิรันดร์ ซึ่งเป็น ปัญหา co-NP- complete หากอนุญาตให้ใช้ตัวบ่งปริมาณทั้งสองจำนวนเท่าใดก็ได้ ปัญหาดังกล่าวเรียกว่าปัญหาของสูตรบูลีนที่มีตัวบ่งปริมาณ ( QBF ) ซึ่งสามารถแสดงให้เห็นได้ว่าเป็น ปัญหา ที่สมบูรณ์แบบในระดับ PSPACEเป็นที่เชื่อกันอย่างกว้างขวางว่าปัญหาที่สมบูรณ์แบบในระดับ PSPACE นั้นยากกว่าปัญหาใดๆ ในกลุ่ม NP อย่างเคร่งครัด แม้ว่ายังไม่มีการพิสูจน์อย่างเป็นทางการก็ตาม

ข้อสอบ SAT ทั่วไปถามว่ามีการกำหนดค่าตัวแปรอย่างน้อยหนึ่งค่าที่ทำให้สูตรเป็นจริงหรือไม่ ส่วนข้อสอบแบบอื่น ๆ จะเกี่ยวข้องกับจำนวนของการกำหนดค่าตัวแปรดังกล่าว:

• MAJ-SATถามว่าอย่างน้อยครึ่งหนึ่งของการมอบหมายทั้งหมดทำให้สูตรเป็นจริงหรือไม่ เป็นที่ทราบกันว่าสมบูรณ์สำหรับPPซึ่งเป็นคลาสความน่าจะเป็น น่าประหลาดใจที่MAJ-kSATได้รับการพิสูจน์แล้วว่าอยู่ใน P สำหรับจำนวนเต็มจำกัด k ทุกตัว^{[ 26 ]}
• #SATซึ่งเป็นปัญหาเกี่ยวกับการนับจำนวนการกำหนดค่าตัวแปรที่สอดคล้องกับสูตร เป็นปัญหาการนับ ไม่ใช่ปัญหาการตัดสินใจ และเป็นปัญหา #P- complete
• UNIQUE SAT ^{[ 27 ]}คือปัญหาในการพิจารณาว่าสูตรมีการกำหนดค่าเพียงหนึ่งเดียวหรือไม่ เป็นปัญหาที่สมบูรณ์สำหรับ^{US [} 28 ] ^{ซึ่งเป็น}คลาสความซับซ้อน ที่อธิบายปัญหาที่สามารถแก้ไขได้โดย เครื่องจักรทัวริงแบบไม่กำหนดเวลาพหุนามที่ยอมรับเมื่อมีเส้นทางการยอมรับแบบไม่กำหนดเพียงหนึ่งเดียวและปฏิเสธในกรณีอื่น ๆ
• UNAMBIGUOUS-SATคือชื่อที่ใช้เรียกปัญหาความพึงพอใจเมื่อสูตรอินพุตรับประกันว่าจะมีการกำหนดค่าที่น่าพอใจได้ไม่เกินหนึ่งรายการ ปัญหานี้เรียกอีกอย่างว่าUSAT [ ^{29 ] อั}ลกอริทึมการแก้ปัญหาสำหรับ UNAMBIGUOUS-SAT สามารถแสดงพฤติกรรมใดๆ ก็ได้ รวมถึงการวนลูปไม่รู้จบ บนสูตรที่มีการกำหนดค่าที่น่าพอใจหลายรายการ แม้ว่าปัญหานี้จะดูง่ายกว่า แต่ Valiant และ Vazirani ได้แสดงให้เห็น^{[ 30 ]}ว่าหากมีอัลกอริทึมที่ใช้งานได้จริง (เช่นอัลกอริทึมเวลาพหุนามแบบสุ่ม ) เพื่อแก้ปัญหานี้ ปัญหาทั้งหมดในNPก็สามารถแก้ไขได้ง่ายเช่นกัน
• MAX-SATหรือปัญหาความสามารถในการทำให้เป็นจริงสูงสุดเป็น ปัญหาที่ขยายมาจาก SAT ไปสู่ ​​FNPโดยถามถึงจำนวนข้อความสูงสุดที่สามารถทำให้เป็นจริงได้ด้วยการกำหนดค่าใดๆ ปัญหานี้มีอัลกอริธึมประมาณค่า ที่มีประสิทธิภาพ แต่การแก้ปัญหาอย่างแม่นยำนั้นยากในระดับ NP-hard ยิ่งไปกว่านั้น มันยังเป็นปัญหาAPX -complete ซึ่งหมายความว่าไม่มีวิธีการประมาณค่าแบบใช้เวลาพหุนาม (PTAS) สำหรับปัญหานี้ เว้นแต่ว่า P=NP
• WMSATคือปัญหาของการค้นหาการกำหนดค่าที่มีน้ำหนักน้อยที่สุดซึ่งสอดคล้องกับสูตรบูลีนแบบโมโนโทน (กล่าวคือ สูตรที่ไม่มีการปฏิเสธใดๆ) น้ำหนักของตัวแปรเชิงประพจน์จะถูกกำหนดไว้ในข้อมูลนำเข้าของปัญหา น้ำหนักของการกำหนดค่าคือผลรวมของน้ำหนักของตัวแปรจริง ปัญหาดังกล่าวเป็น NP-complete (ดูทฤษฎีบทที่ 1 ของ^{[ 31 ]} )

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

แม้ว่า SAT จะเป็นปัญหาการตัดสินใจแต่ปัญหาการค้นหาการกำหนดค่าที่น่าพอใจนั้นลดรูปไปเป็น SAT กล่าวคือ อัลกอริทึมแต่ละตัวที่ตอบคำถามได้อย่างถูกต้องว่าอินสแตนซ์ของ SAT สามารถแก้ไขได้หรือไม่ สามารถนำมาใช้เพื่อค้นหาการกำหนดค่าที่น่าพอใจได้ ขั้นแรก จะถามคำถามกับสูตร Φ ที่กำหนดให้ ถ้าคำตอบคือ "ไม่" แสดงว่าสูตรนั้นไม่สามารถหาคำตอบได้ มิฉะนั้น จะถามคำถามกับสูตรที่กำหนดค่าบางส่วนแล้ว Φ { x ₁ =TRUE}นั่นคือ Φ ที่แทนที่ตัวแปรแรกx ₁ด้วย TRUE และลดรูปตามนั้น ถ้าคำตอบคือ "ใช่" แสดงว่าx ₁ =TRUE มิฉะนั้นx ₁ =FALSE ค่าของตัวแปรอื่นๆ สามารถหาได้ในภายหลังด้วยวิธีเดียวกัน โดยรวมแล้วต้องใช้การทำงานของอัลกอริทึมn + 1 ครั้ง โดยที่ nคือจำนวนตัวแปรที่แตกต่างกันใน Φ

คุณสมบัตินี้ถูกนำไปใช้ในทฤษฎีบทหลายข้อในทฤษฎีความซับซ้อน:

• NP ⊆ P/poly ⇒ PH = Σ ₂ ( ทฤษฎีบทคาร์ป-ลิปตัน )
• NP ⊆ BPP ⇒ NP = RP
• P = NP ⇒ FP = FNP

เนื่องจากปัญหา SAT เป็นปัญหา NP-complete จึงมีเพียงอัลกอริทึมที่มีความซับซ้อนในกรณีที่เลวร้ายที่สุดแบบเลขชี้กำลังเท่านั้นที่เป็นที่รู้จัก แม้จะเป็นเช่นนั้น อัลกอริทึมที่มีประสิทธิภาพและปรับขนาดได้สำหรับ SAT ก็ได้รับการพัฒนาในช่วงทศวรรษ 2000 และมีส่วนช่วยให้เกิดความก้าวหน้าอย่างมากในความสามารถในการแก้ปัญหาโดยอัตโนมัติซึ่งเกี่ยวข้องกับตัวแปรหลายหมื่นตัวและข้อจำกัดหลายล้านข้อ (เช่น ข้อความ) ^{[ 3 ]}ตัวอย่างของปัญหาดังกล่าวในการออกแบบระบบอิเล็กทรอนิกส์อัตโนมัติ (EDA) ได้แก่ การตรวจ สอบความเท่าเทียมกันอย่างเป็นทางการ การตรวจสอบแบบ จำลองการตรวจสอบอย่างเป็นทางการของไมโครโปรเซสเซอร์แบบไปป์ไลน์ [ ^{25 ]}การสร้างรูปแบบการทดสอบอัตโนมัติการกำหนดเส้นทางของFPGA [ ^{32 ]}การวางแผน^และ ปัญหาการจัดตารางเวลาเป็นต้น เครื่องมือแก้ปัญหา SAT ยังถือเป็นส่วนประกอบที่สำคัญใน^{กล่อง}เครื่องมือ การออกแบบระบบอิเล็กทรอนิกส์อัตโนมัติ อีกด้วย

เทคนิคหลักที่ใช้โดยตัวแก้ปัญหา SAT สมัยใหม่ ได้แก่อัลกอริทึม Davis–Putnam–Logemann–Loveland (หรือ DPLL), การเรียนรู้ข้อความที่ขับเคลื่อนด้วยความขัดแย้ง (CDCL) และ อัลกอริทึม การค้นหาเฉพาะที่แบบสุ่ม เช่นWalkSATตัวแก้ปัญหา SAT เกือบทั้งหมดมีการกำหนดเวลาหมดอายุ ดังนั้นจะยุติในเวลาที่เหมาะสมแม้ว่าจะไม่สามารถหาคำตอบได้ก็ตาม ตัวแก้ปัญหา SAT ที่แตกต่างกันจะพบว่าอินสแตนซ์ต่างๆ ง่ายหรือยากต่างกัน และบางตัวก็เก่งในการพิสูจน์ความไม่สามารถพอใจได้ ในขณะที่บางตัวก็เก่งในการหาคำตอบ ความพยายามล่าสุดได้เกิดขึ้นเพื่อเรียนรู้ความสามารถในการพอใจของอินสแตนซ์โดยใช้เทคนิคการเรียนรู้เชิงลึก^{[ 33 ]}

โปรแกรมแก้ปัญหา SAT ได้รับการพัฒนาและเปรียบเทียบในการแข่งขันแก้ปัญหา SAT ^{[ 34 ]}โปรแกรมแก้ปัญหา SAT สมัยใหม่ยังมีผลกระทบอย่างมากต่อสาขาการตรวจสอบซอฟต์แวร์ การแก้ปัญหาข้อจำกัดในปัญญาประดิษฐ์ และการวิจัยการดำเนินงานเป็นต้น

ในช่วงหลายทศวรรษที่ผ่านมา มีการนำเสนออัลกอริทึมเชิงทฤษฎีที่มีการรับประกันเวลาการทำงานในกรณีที่เลวร้ายที่สุดที่ดีขึ้นเรื่อยๆ รวมถึง อัลกอริทึมสำหรับชุดข้อความที่มีความยาว ⁽จำนวนตัวอักษรทั้งหมด) [ ^{35 ] [ 36 ]} อัลกอริทึมสำหรับชุดของข้อความ^{[ 37 ] [ 38 ]}และอัลกอริทึมสำหรับ 3-SAT ที่มีตัวแปร^{[ 39 ]}ในที่นี้ สัญลักษณ์ " " หมายถึง "จนถึงตัวประกอบพหุนาม" เช่นการรับประกันเวลาการทำงานก่อนหน้านี้แสดงอยู่ในแผนภาพ ${\displaystyle O^{*}(1.0638^{L})}$${\displaystyle L}$${\displaystyle O^{*}(1.2226^{m})}$${\displaystyle m}$${\displaystyle O^{*}(1.32793^{n})}$${\displaystyle n}$${\displaystyle O^{*}(.)}$${\displaystyle O^{*}(f(n))=O(f(n)n^{O(1)})}$

• แกนกลางที่ไม่อาจพึงพอใจ
• ความพึงพอใจตามทฤษฎี
• การนับคะแนน SAT
• แพลนาร์ เอสเอที
• อัลกอริทึม Karloff–Zwick
• ความสามารถในการตอบสนองของวงจร

• เกม SAT : ลองแก้ปัญหาความพึงพอใจแบบบูลีนด้วยตัวคุณเอง
• เว็บไซต์การแข่งขัน SAT ระดับนานาชาติ
• การประชุมวิชาการนานาชาติว่าด้วยทฤษฎีและการประยุกต์ใช้การทดสอบความน่าพอใจ
• วารสารว่าด้วยความพึงพอใจ การสร้างแบบจำลองบูลีน และการคำนวณ
• SAT Live คือเว็บไซต์รวบรวมข้อมูลการวิจัยเกี่ยวกับปัญหาความน่าพอใจ (satisfiability problem)
• การประเมินผลประจำปีของผู้แก้โจทย์ MaxSAT

• บทความนี้มีเนื้อหาจากhttps://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.htmlโดยศาสตราจารย์Karem A. Sakallah

(เรียงตามวันที่ตีพิมพ์)