Существует ли название для сценария решения SAT, в котором часть формулы является статической (формирует пропозициональную «теорию») и служит статическим контекстом для проверки выполнимости относительно небольшого предложения.
Многие такие тесты должны быть выполнены с другим предложением, поэтому оценка соединения каждой маленькой формулы со статической частью каждый раз заново неоптимальна.
В отличие от инкрементального SAT, выполнимые предложения не добавляются к теории, а отбрасываются после тестирования.
Есть ли инструмент, который можно адаптировать для такого случая?