我试图编译一个名为 CADET 的 QBF 求解器工具。CADET 只能解决 QDIMACS 的格式类型。
克隆存储库并安装工具后，只需一个简单的命令即可。./cadet <filename>.qdimacs需要执行该文件。给出了错误的照片和 QDIMACS 文件。
这是 .qdimacs 文件代码
c This QDIMACS file encodes the formula
c forall x1, x2 exists y. y <-> x1 & x2.
c x1 is represented by number 1
c x2 is represented by number 2
c y is represented by number 3
p cnf 3 3
a 1 2 0
e 3 0
1 -3 0
2 -3 0
-1 -2 3 0
这是我在执行期间收到的警告：
harish@harish-Lenovo-ideapad-510-15IKB:~/cadet$ ./cadet harish.qdimacs
CADET v2.5
Processing file "harish.qdimacs".
Warning: Quantifier hierarchy ended with a universal quantifier.
Warning: Removing last quantifier. Will obtain a propositional problem. This is a bit hacky, so beware.
Aborted (core dumped)