Z3 Forall พร้อมอาร์เรย์

Question

Z3 ไม่ทราบปัญหาง่ายๆ:

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

ฉันพบว่ามันกลายเป็น sat ถ้าลบล้างforallแต่ดูเหมือนว่าจะเป็นเรื่องง่ายๆที่ไม่สามารถแก้ไขได้

สิ่งนี้ก่อให้เกิดปัญหาเนื่องจากระดับของปัญหาที่ฉันต้องการแก้ไขมีมากกว่าเช่น

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

ในกรณีที่การปฏิเสธ forall เพียงอย่างเดียวไม่ใช่ปัญหาเดียวกันดังนั้นจึงไม่สามารถทำได้ที่นี่ มีวิธีใดบ้างในการสร้างปัญหาลักษณะนี้กับ Z3 เพื่อให้ได้ผลลัพธ์ที่ไม่ / sat?

Answer 1

ปัญหาเกี่ยวกับตัวระบุปริมาณมักเป็นปัญหากับตัวแก้ SMT โดยเฉพาะอย่างยิ่งหากพวกเขาเกี่ยวข้องกับอาร์เรย์และตัวระบุปริมาณแบบสลับเช่นในตัวอย่างของคุณ exits u. forall y. P(u, y)คุณเป็นหลักมี Z3 หรือโปรแกรมแก้ปัญหา SMT อื่น ๆ จะมีปัญหาในการจัดการกับปัญหาประเภทนี้

เมื่อคุณมีการยืนยันเชิงปริมาณเช่นเดียวกับที่คุณทำในที่ที่คุณมีforallอยู่ในระดับบนสุดหรือซ้อนกันexistsตรรกะจะกลายเป็นกึ่งตัดสินใจได้ Z3 ใช้ MBQI (model-based quantifier instantiation) เพื่อแก้ปัญหาดังกล่าวในเชิงฮิวริสติก แต่ก็มักจะไม่ทำเช่นนั้น ปัญหาไม่ได้เป็นเพียงแค่ z3 ไม่สามารถทำได้: ไม่มีขั้นตอนการตัดสินใจสำหรับปัญหาดังกล่าวและ z3 ทำได้ดีที่สุด

คุณสามารถลองให้รูปแบบตัวบ่งชี้สำหรับปัญหาดังกล่าวเพื่อช่วย z3 ได้ แต่ฉันไม่เห็นวิธีง่ายๆในการนำไปใช้กับปัญหาของคุณ (รูปแบบควอนตัมใช้เมื่อคุณมีฟังก์ชันที่ไม่ได้ตีความและสัจพจน์เชิงปริมาณดูhttps://rise4fun.com/z3/tutorialcontent/guide#h28). ฉันไม่คิดว่ามันจะเหมาะกับคุณ แม้ว่าจะเป็นเช่นนั้นรูปแบบก็เป็นสิ่งที่พิถีพิถันในการเขียนโปรแกรมและไม่ได้มีประสิทธิภาพเมื่อเทียบกับการเปลี่ยนแปลงข้อกำหนดของคุณที่อาจดูไม่มีพิษภัย

หากคุณกำลังจัดการกับตัวระบุจำนวนดังกล่าวตัวแก้ SMT อาจไม่เหมาะ มองหาผู้พิสูจน์ทฤษฎีบทกึ่งอัตโนมัติเช่น Lean, Isabelle, Coq เป็นต้นซึ่งออกแบบมาเพื่อจัดการกับตัวระบุปริมาณในวิธีที่มีระเบียบวินัยมากขึ้น แน่นอนว่าคุณสูญเสียระบบอัตโนมัติเต็มรูปแบบ แต่เครื่องมือเหล่านี้ส่วนใหญ่สามารถใช้ตัวแก้ SMT เพื่อปลดปล่อยเป้าหมายย่อยที่ "ง่าย" เพียงพอ ด้วยวิธีนี้คุณยังคงทำการ "ยกของหนัก" ด้วยตนเอง แต่เป้าหมายย่อยส่วนใหญ่จะจัดการโดยอัตโนมัติโดย z3 (โดยเฉพาะอย่างยิ่งในกรณีของ Lean โปรดดูที่นี่:https://leanprover.github.io/)

Answer 2

มีวงเล็บปิด (ขวา) พิเศษ 1 อันซึ่งจำเป็นต้องลบออก นอกจากนี้ให้เพิ่มการยืนยันก่อนคำสั่ง forall

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

เรียกใช้รหัสด้านบนและคุณจะได้รับ unsat เป็นคำตอบ

สำหรับโปรแกรมที่สองคำตอบของนามแฝงอาจเป็นประโยชน์สำหรับคุณ