В компании, в которой я работаю, у нас есть доступ к нескольким SAT Solvers. Мы хотели бы проанализировать, как каждый решатель SAT влияет на производительность решателя Z3 SMT.
Можно ли из Z3 вызвать внешний SAT-решатель? Если нет, то где следует изменить Z3 для вызова внешнего решателя?
Я не думаю, что это будет легкой задачей, потому что Z3 использует тесно интегрированный внутренний SAT-решатель. Необходимая тесная интеграция с решателем SAT означает, что Z3 должен будет взаимодействовать через низкоуровневый API внешнего решателя SAT, например. с функцией push и pop. Эти API не стандартизированы, поэтому задача интеграции, например. с MiniSat будет отличаться от, например, задача интеграции с Lingeling. Я не говорю, что это невозможно, потому что Z3 имеет модульную архитектуру, которая предназначена для расширения, но я думаю, что это потребует серьезных усилий.
Возможно, появится один из разработчиков Z3 и докажет, что я ошибаюсь.
