DPLL (T) вообще не используется для решения проблем QF_BV.Комментарий к статье «Эффективное решение квантованных формул битовых векторов» о Z3 2.x.QF_BV это все о проблемном кодировании.Предварительная обработка имеет большое значение.Я построил новый стек предварительной обработки и SAT Solver с нуля для Z3 3.0.Новый препроцессор намного быстрее, чем используемый в Z3 2.x, и выполняет более агрессивные упрощенияЗдесь нет ни магии, ни причудливых техник.После шага предварительной обработки, Z3 обрабатывает все и запускает новый SAT-решатель.Z3 не использует заниженную / пониженную аппроксимацию для битовых векторов, арифметические рассуждения на уровне слов или специальную поддержку нелинейных операторов.Кстати, одна вещь, которую мало кто решает принять во внимание, состоит в том, что некоторые упрощения могут уменьшить размер формулы локально, но увеличить ее глобально, потому что они разрушают совместное использование.Z3 также использует шаг предварительной обработки, который пытается увеличить степень совместного использования в линейной и нелинейной бит-векторной арифметике.