Логики SMT с плавающей точкой медленнее реальных?

Question

Я написал приложение на Haskell, которое вызывает решатель Z3 для решения ограничений с помощью некоторых сложных формул. Благодаря Haskell я могу быстро переключать тип данных, с которыми я работаю.

При использовании SBV AlgReal типа для вычислений, я получаю результаты в разумное время, однако переключаясь на Float или же Double Типы заставляют Z3 потреблять ~2 ГБ ОЗУ и не приводят даже к 30 минутам.

Ожидается ли это, что создание решений с плавающей запятой требует гораздо больше времени, или это какая-то ошибка с моей стороны?

Answer 1

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

Здесь также есть риск сравнения яблок с апельсинами: Reals и float - это две совершенно разные логики, с разными процедурами принятия решений, эвристикой, алгоритмами и т. Д. Я уверен, что вы можете найти проблемы, когда один превосходит другой, без ясного победитель "производительности".

Сказав все это, вот некоторые вещи, которые делают с плавающей точкой (FP) сложно:

• Переписывание почти невозможно с FP, так как такие правила, как ассоциативность, просто не выполняются для сложения / умножения FP. Таким образом, существует меньше возможностей для упрощения перед дробеструйной обработкой.

• так же a * 1/a == 1 не держится за поплавки. Ни один не делает x + 1 /= x или же (x + a == x) -> (a == 0) и много других "очевидных" упрощений, которые вы хотели бы сделать. Все это усложняет рассуждения.

• Существование NaN значения делают равенство неотражающим: ничто не может сравниться с NaN включая себя. Таким образом, замена равных для равных также проблематична и требует дополнительных условий.

• Аналогично, существование +0 а также -0, которые сравнивают равные, но ведут себя по-разному из-за округления усложняют дела. Типичный пример x == 0 -> fma(a, b, x) == a * b не держит (где fma является слитым умножением-сложением), поскольку в зависимости от знака нуля эти два выражения могут давать разные значения для разных режимов округления.

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

• Такие операции, как умножение, деление и остаток (да, есть операция с плавающей запятой!) По своей природе очень сложны и приводят к чрезвычайно большим формулам SAT. В частности, умножение является известной операцией, которая бросает вызов большинству SAT/BDD-движков из-за отсутствия каких-либо хороших эвристических методов упорядочения и разделения. Решающие задачи в конечном итоге обрабатываются достаточно быстро, что приводит к очень большим пространствам состояний. Я заметил, что решающим людям трудно иметь дело с операциями деления и остатка FP, даже когда ввод является полностью конкретным, представьте себе, что происходит, когда они полностью символичны!

• Логика вещественных чисел имеет процедуру принятия решения с двойной экспоненциальной сложностью. Однако такие методы, как устранение Фурье-Моцкина ( https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination), оставаясь экспоненциальными, на практике работают очень хорошо.

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

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

Хорошая статья о том, как обрабатывать поплавки IEEE754 в решателях SMT: http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf. Вы можете увидеть множество операций, которые он поддерживает, и почувствовать сложность.