В общем, решатели SMT могут обрабатывать множество интересующих теорий: целые числа, действительные числа, строки, последовательности, множества, неинтерпретированные функции, типы данных, рекурсивные определения, линейные и нелинейные арифметики. 1002 * Вы можете взглянуть на http://smtlib.cs.uiowa.edu/logics.shtml, чтобы увидеть общую поддерживаемую логику. Решатели SMT сияют тем, что вы можете свободно смешивать и сопоставлять ограничения из этих доменов в одной общей структуре.
Я не очень хорошо знаком с Gecode, но полагаю, что он гораздо более сфокусирован, глядя только на класс ограничений. Это, конечно, сделало бы его очень мощным для области, для которой оно предназначено, но также означало бы, что у них нет универсальности, предлагаемой решателями SMT.
Если вы пытаетесь «выбрать» один, Я бы рекомендовал принимать решение в индивидуальном порядке: для каждой проблемы вы можете обнаружить, что победителем может быть SMT-решатель или какой-либо другой решатель ограничений, который не основан на SMT-технологии. Я сомневаюсь, что вы можете «однозначно» выбрать одно из них для любой проблемы, которая может у вас возникнуть. Если вы разместите конкретные c -вопросы, которые вас интересуют, вы сможете получить лучшие предложения.