นี่คือคำสั่ง depqbf ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
depqbf - ตัวแก้สำหรับสูตรบูลีนเชิงปริมาณ
เรื่องย่อ
เดพคิวบ์ [ตัวเลือก ... ] [NUM] [ไฟล์]
DESCRIPTION
เดพคิวบ์ เป็นตัวแก้ปัญหาตามการค้นหาสำหรับสูตรบูลีนเชิงปริมาณ (QBF) ในprenex
รูปแบบปกติที่เชื่อมต่อกัน มันขึ้นอยู่กับอัลกอริทึม DPLL สำหรับ QBF ที่มีการขับเคลื่อนด้วยความขัดแย้ง
การเรียนรู้คิวบ์ที่ขับเคลื่อนด้วยประโยคและโซลูชัน โดยการวิเคราะห์โครงสร้างของสูตร DepQBF
พยายามระบุตัวแปรอิสระ นอกจากประโยชน์อื่นๆแล้ว มักจะ
เพิ่มอิสระในการตัดสินใจ ดูคำอธิบายระบบ JSAT ของ DepQBF 0.1 . ด้วย
จาก QBFEVAL'10 เพื่อใช้อ้างอิงและสรุปแนวคิดโดยย่อ
เดพคิวบ์ อ่านสูตร QBF ในรูปแบบ QDIMACS ถ้า ไฟล์ ไม่ได้รับมันอ่านอินพุตจาก
มาตรฐาน เป็นไปตามมาตรฐานอินพุต/เอาต์พุตตามที่กำหนดโดย QBFEVAL'10
OPTIONS
เดพคิวบ์ ยอมรับตัวเลือกต่อไปนี้:
-ชม, --ช่วยด้วย
พิมพ์ข้อมูลการใช้งาน
--รุ่น
รุ่นพิมพ์.
--สวย-พิมพ์
แยกวิเคราะห์และพิมพ์สูตรเท่านั้น
-v เพิ่มความฟุ่มเฟือยไปเรื่อย ๆ
NUM ไม่บังคับ: หมดเวลาหลังจาก NUM วินาที
ไฟล์ ทางเลือก: อ่านอินพุตจาก FILE
EXIT สถานภาพ
สถานะการออกคือ 10 หากสูตร QBF ที่กำหนดเป็นอินพุตเป็นที่พอใจ และ 20 หากเป็น
ไม่น่าพอใจ; รหัสออกอื่นใดบ่งชี้ว่าสูตรไม่ได้รับการแก้ไข
ใช้ depqbf ออนไลน์โดยใช้บริการ onworks.net
