Для каких именно квантификаторов подходит SMT?

Есть две категории количественных формул, для которых CVC4 является полным.

(1) Квантовые формулы с конечными областями определения.

CVC4 является конечно-модельно-полной для кванторов неинтерпретируемых сортировок, а это означает, что если существует модель, в которой все неинтерпретируемые сортировки интерпретируются как конечные, то CVC4 в конечном итоге ее найдет. Подробнее см. в этом документе:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
, где кратко изложены материалы конференции:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Обратите внимание, что эти методы сочетаются с любой теорией, поддерживаемой CVC4. При условии, что теория разрешима и количественная оценка не включает (бесконечные) интерпретируемые сорта, гарантия конечной модельной полноты остается.

Этот подход также обеспечивает полное опровержение для определенных фрагментов, таких как фрагмент Бернайса-Шенфинкеля-Рамси (ЭПР), что означает, что для любой неразрешимой проблемы в этом фрагменте CVC4 в конечном итоге ответит «неудовлетворительно».

Если вас интересует эта функция, CVC4 по умолчанию не будет использовать поиск конечной модели для входной задачи. Параметр командной строки "--finite-model-find" активирует эти методы.

(2) Кванторные формулы в некоторых теориях, использующих исключение кванторов.

Например, CVC4 является полным для (чистой) количественной линейной арифметики. Подробнее см. в этом документе:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
, который основан на более раннем документе конференции:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

По духу это похоже на другие подходы, например, в Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Рискуя бесполезно не ответить на вопрос, есть причины, по которым этот материал трудно найти.

Связь между разрешимостью и «на самом деле может решить мою конкретную проблему за то время, которое я готов ждать» не так уж сильна. Поэтому часто примеры, наборы тестов и результаты экспериментов являются лучшим индикатором (и поэтому представлены).

Кроме того, большинство решателей проводят некоторое количество эвристических переписываний и манипуляций с проблемами, прежде чем пытаться решить. Таким образом, классические синтаксические способы выражения разрешимых фрагментов не всегда применимы, поскольку другие проблемы могут быть переписаны в разрешимые (надеюсь, не наоборот, но я не могу обещать, что этого никогда не произойдет!).

Наконец, многие решатели используют эвристические полурешающие процедуры, которые хорошо работают, но их трудно описать чем-то более формальным, чем код. Таким образом, есть вещи, которые могут не появиться ни в одном известном разрешимом фрагменте, но для которых можно найти ответы.