Я пытался скомпилировать инструмент решения QBF под названием CADET. 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)