Universal Quantifiers ใน QBF

Question

ฉันได้ตรวจสอบการลด / ออกจากภาษา TQBF และได้จัดการกับสิ่งที่เกือบจะไม่เป็นความจริงอย่างแน่นอน (หรือถ้าเป็นความจริงฉันก็ขาดต้นทุนการคำนวณที่สำคัญที่เกี่ยวข้อง) เกี่ยวกับการทำให้ง่ายขึ้น อินสแตนซ์ TQBF

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

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee c)\wedge (\neg b \vee \neg c \vee d)\wedge (a \vee c \vee \neg d)$

อันดับแรกฉันยืนยันว่าอินสแตนซ์นี้ไม่น่าพอใจ (ตรวจสอบได้ง่ายด้วยมือ) หากเราใช้วิธีการที่ฉันอธิบายข้างต้นเราจะได้รับ "core" ดังต่อไปนี้:

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee c)\wedge (\neg c) \wedge (a \vee c)$

ซึ่งเห็นได้ชัดว่าไม่น่าพอใจ หากแทนที่จะเป็นตัวอย่างนี้เราจะดูสิ่งนี้:

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee \neg c)\wedge (\neg b \vee c \vee d)\wedge (a \vee c \vee \neg d)$

ซึ่งเป็นที่น่าพอใจอย่างชัดเจน (ตั้งค่า c เป็นจริง a เป็นเท็จ) และมี "แกน" ของ

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee \neg c)\wedge (c) \wedge (a \vee c)$

ซึ่งเป็นที่น่าพอใจด้วยการตั้งค่าตัวแปรเดียวกัน

หากวิธีนี้ใช้ได้ผลเสมอดูเหมือนว่าจะมีการลดลงจาก TQBF เป็น SAT ในเชิงเส้นเวลาในจำนวนตัวบ่งชี้สากลและจำนวนการเกิดขึ้นของตัวแปรเชิงปริมาณสากลในสูตรซึ่งแสดงให้เห็นว่า TQBF เป็น NP-Complete (เป็นที่ทราบกันดีอยู่แล้วว่าเป็น PSPACE-Complete และเป็น NP-Hard ดังนั้นหากอยู่ใน NP จะเป็น NP-Complete) และยิ่งไปกว่านั้น NP = PSPACE ฉันจะตะลึงมากถ้าเป็นกรณีนี้ แต่ฉันไม่สามารถหาตัวอย่างตอบโต้ได้ (หรือค่าใช้จ่ายในการคำนวณที่ขาดหายไปในการลดลงซึ่งทำให้ไม่ใช่เวลาพหุนาม) ฉันขาดอะไรไป?

Answer 1

สัญชาตญาณของคุณถูกต้อง มันใช้ไม่ได้ นี่คือตัวอย่างการตอบโต้

พิจารณา $\forall a \exists b \varphi(a,b)$ ที่ไหน $\varphi(a,b) = (a \lor \neg b) \land (\neg a \lor b)$. คำสั่งนี้ประเมินว่าเป็นจริง

อย่างไรก็ตามหากเรานำออก $a$ ทำตามขั้นตอนของคุณเราได้รับ $\exists b \psi(b)$ ที่ไหน $\psi(b) = ((\neg b) \land (b))$; และคำสั่งนั้นประเมินว่าเป็นเท็จ

วิธีหนึ่งในการทำความเข้าใจว่าทำไมวิธีของคุณถึงไม่ได้ผลก็คือ $\forall a \exists b \varphi(a,b)$ ไม่เทียบเท่ากับ $\exists b \forall a \varphi(a,b)$. วิธีการส่วนใหญ่ของคุณอาจใช้ได้ผลถ้าไฟล์$\forall$อยู่ด้านในกล่าวคือสำหรับประโยคของรูปแบบ $\exists \cdots \exists \forall \cdots \forall$แต่ไม่ใช่สำหรับรูปแบบอื่น ๆ ของ $\exists$ และ $\forall$.