В настоящее время я использую CVC4 для решения формул следующего вида:
exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
Здесь f1...fn — это функции от некоторого числа от Bool до Bool, а b1...bk — логические значения.
Моя проблема прямо связана с фрагментом UF SMT: в нем есть квантификаторы, но нет сортировок, кроме функций и логических значений.
Когда я пробую свою проблему с настройками по умолчанию на CVC4, он сразу же возвращает Неизвестно, несмотря на то, что вся моя количественная оценка выполняется по конечным доменам.
Проблема в том, что CVC4 имеет чрезвычайно большое количество вариантов работы с квантификаторами: есть куча cegqi, куча fmf, есть mbqi и т. д. У меня такое впечатление, что большинство из них были добавлены из конкретных исследовательских проектов, и я бы предпочел не читать 20 различных статей только для того, чтобы найти свое решение.
Мой вопрос: есть ли рекомендуемый набор вариантов для решения подобных проблем?
Я знаю, что это возможно с CVC4, так как они конкурировали и показали хорошие результаты на UF Отслеживание конкурса SMT, но я не могу найти конкретные аргументы, используемые для этого конкурса.
