ในวิทยาการคอมพิวเตอร์เชิงทฤษฎีปัญหาความสามารถในการทำให้วงจร เป็นจริง (หรือที่รู้จักกันในชื่อCIRCUIT-SAT , CircuitSAT , CSATเป็นต้น) คือปัญหาการตัดสินใจในการพิจารณาว่าวงจรบูลีน ที่กำหนด มีการกำหนดค่าอินพุตที่ทำให้เอาต์พุตเป็นจริง หรือไม่ ^{[ 1 ]}กล่าวอีกนัยหนึ่งคือ ถามว่าอินพุตของวงจรบูลีนที่กำหนดสามารถตั้งค่าเป็น1หรือ0 ได้อย่างสม่ำเสมอ หรือไม่ เพื่อให้วงจรส่งออกเป็น 1ถ้าเป็นเช่นนั้น วงจรจะเรียกว่าสามารถทำให้เป็นจริงได้มิฉะนั้น วงจรจะเรียกว่าไม่สามารถทำให้เป็นจริงได้ ในรูปทางด้านขวา วงจรด้านซ้ายสามารถทำให้เป็นจริงได้โดยการตั้งค่าอินพุตทั้งสองเป็น1แต่วงจรด้านขวาไม่สามารถทำให้เป็นจริงได้

CircuitSAT มีความเกี่ยวข้องอย่างใกล้ชิดกับปัญหาความพึงพอใจของบูลีน (SAT)และเช่นเดียวกัน ได้รับการพิสูจน์แล้วว่าเป็นปัญหาNP-complete ^{[ 2 ]}มันเป็นปัญหา NP-complete ต้นแบบทฤษฎีบท Cook–Levinบางครั้งได้รับการพิสูจน์บน CircuitSAT แทนที่จะเป็นบน SAT จากนั้น CircuitSAT สามารถลดรูปเป็นปัญหาความพึงพอใจอื่นๆ เพื่อพิสูจน์ความเป็น NP-complete ของปัญหาเหล่านั้น^{[ 1 ] [ 3 ]}ความพึงพอใจของวงจรที่มีเกตไบนารีแบบใดก็ได้สามารถตัดสินได้ในเวลา^{[ 4 ]}${\displaystyle m}$${\displaystyle O(2^{0.4058m})}$

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

สมมติว่าสูตร 3SAT ดั้งเดิมมีตัวแปร, และตัวดำเนินการ (AND, OR, NOT) จงออกแบบวงจรที่มีอินพุตที่สอดคล้องกับตัวแปรแต่ละตัวและเกตที่สอดคล้องกับตัวดำเนินการแต่ละตัว เชื่อมต่อเกตตามสูตร 3SAT ตัวอย่างเช่น ถ้าสูตร 3SAT คือวงจรจะมีอินพุต 3 ตัว เกต AND หนึ่งตัว เกต OR หนึ่งตัว และเกต NOT หนึ่งตัว อินพุตที่สอดคล้องกับจะถูกกลับค่าก่อนส่งไปยังเกต AND ที่มีและเอาต์พุตของเกต AND จะถูกส่งไปยังเกต OR ที่มี${\displaystyle x_{1},x_{2},\dots ,x_{n}}$${\displaystyle y_{1},y_{2},\dots ,y_{k}}$${\displaystyle (\lnot x_{1}\land x_{2})\lor x_{3},}$${\displaystyle x_{1}}$${\displaystyle x_{2},}$${\displaystyle x_{3}.}$

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

นี่เป็นการพิสูจน์เสร็จสมบูรณ์ว่าวงจร SAT เป็นปัญหา NP-Complete

สมมติว่าเราได้รับวงจรบูลีนแบบระนาบ (กล่าวคือ วงจรบูลีนที่มีกราฟพื้นฐานเป็นแบบระนาบ ) ซึ่งประกอบด้วย เกต NAND เท่านั้น ที่มีอินพุตสองตัวพอดี ปัญหา SAT ของวงจรแบบระนาบคือปัญหาการตัดสินใจในการพิจารณาว่าวงจรนี้มีการกำหนดอินพุตที่ทำให้เอาต์พุตเป็นจริงหรือไม่ ปัญหานี้เป็นปัญหา NP-complete ยิ่งไปกว่านั้น หากมีการเปลี่ยนแปลงข้อจำกัดเพื่อให้เกตใดๆ ในวงจรเป็น เกต NORปัญหาที่ได้ก็ยังคงเป็นปัญหา NP-complete อยู่^{[ 5 ]}

ปัญหา Circuit UNSAT คือปัญหาการตัดสินใจในการพิจารณาว่าวงจรบูลีนที่กำหนดให้ส่งค่าเป็นเท็จหรือไม่ สำหรับการกำหนดค่าอินพุตที่เป็นไปได้ทั้งหมด ปัญหานี้เป็นส่วนเติมเต็มของปัญหา Circuit SAT และดังนั้นจึงเป็นปัญหาco-NP- complete

การลดรูปจาก CircuitSAT หรือรูปแบบต่างๆ ของมัน สามารถนำมาใช้เพื่อแสดงให้เห็นถึงความยากแบบ NP-hard ของปัญหาบางอย่าง และเป็นทางเลือกอื่นนอกเหนือจากการลดรูปตรรกะแบบ dual-rail และ binary logic อุปกรณ์ที่จำเป็นสำหรับการลดรูปดังกล่าวมีดังนี้:

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

ปัญหานี้ถามว่าสามารถระบุตำแหน่งของระเบิดทั้งหมดบน กระดาน Minesweeper ได้หรือ ไม่ ได้มีการพิสูจน์แล้วว่าเป็นปัญหาco-NP-completeผ่านการลดรูปจากปัญหาวงจร UNSAT ^{[ 6 ]}อุปกรณ์ที่สร้างขึ้นสำหรับการลดรูปนี้ได้แก่ สายไฟ ตัวแยก เกต AND และ NOT และตัวหยุด^{[ 7 ]}มีข้อสังเกตที่สำคัญสามประการเกี่ยวกับอุปกรณ์เหล่านี้ ประการแรก อุปกรณ์ตัวแยกสามารถใช้เป็นอุปกรณ์ NOT และอุปกรณ์ตัวหมุนได้ ประการที่สอง การสร้างอุปกรณ์ AND และ NOT นั้นเพียงพอแล้ว เพราะเมื่อรวมกันแล้วสามารถจำลองเกต NAND สากลได้ สุดท้าย เนื่องจาก NAND สามตัวสามารถประกอบกันโดยไม่มีจุดตัดเพื่อใช้ XOR และเนื่องจาก XOR นั้นเพียงพอที่จะสร้างครอสโอเวอร์^{[ 8 ]}ทำให้เราได้อุปกรณ์ครอสโอเวอร์ที่ต้องการ

การแปลง Tseytinเป็นการลดรูปโดยตรงจาก Circuit-SAT ไปเป็นSATการแปลงนี้อธิบายได้ง่ายหากวงจรทั้งหมดสร้างขึ้นจากเกต NAND 2 อินพุต ( ชุดตัวดำเนินการบูลีนที่สมบูรณ์ในเชิงฟังก์ชัน ): กำหนดตัวแปรให้กับ เน็ต ทุก ตัวในวงจร จากนั้นสำหรับแต่ละเกต NAND ให้สร้าง ข้อความ รูปแบบปกติแบบเชื่อมโยง ( v ₁ ∨ v ₃ ) ∧ ( v ₂ ∨ v ₃ ) ∧ (¬ v ₁ ∨ ¬ v ₂ ∨ ¬ v ₃ ) โดยที่v ₁และv ₂เป็นอินพุตของเกต NAND และv ₃เป็นเอาต์พุต ข้อความเหล่านี้อธิบายความสัมพันธ์ระหว่างตัวแปรทั้งสามได้อย่างสมบูรณ์ การเชื่อมโยงข้อความจากเกตทั้งหมดเข้ากับข้อความเพิ่มเติมที่จำกัดให้ตัวแปรเอาต์พุตของวงจรเป็นจริงจะทำให้การลดรูปเสร็จสมบูรณ์ การกำหนดตัวแปรที่ตรงตามข้อจำกัดทั้งหมดมีอยู่ก็ต่อเมื่อวงจรดั้งเดิมสามารถหาคำตอบได้ และวิธีแก้ปัญหาใดๆ ก็ตามเป็นวิธีแก้ปัญหาดั้งเดิมของการค้นหาอินพุตที่ทำให้วงจรมีเอาต์พุตเป็น 1 ^{[ 1 ] [ 9 ]}ในทางกลับกัน—ที่ว่า SAT สามารถลดรูปเป็น circuit-SAT ได้—เป็นผลลัพธ์ที่เห็นได้ชัดจากการเขียนสูตรบูลีนใหม่เป็นวงจรและแก้ปัญหา

• ปัญหาค่าวงจร
• ความสามารถในการตอบสนองของวงจรที่มีโครงสร้าง
• ปัญหาความพึงพอใจ