Как и в случае любого вопроса, касающегося производительности решателя, невозможно сделать обобщения.Кристоф Винтерштайгер (https://stackoverflow.com/users/869966/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 относительно новы, и это нишевая область с зарождающейся областьюисследования. Таким образом, существующие решатели имеют тенденцию быть достаточно консервативными и быстро обрабатывать биты и сводить проблему к битовой векторной логике. Я ожидаю, что они улучшатся со временем, как и все другие теории.
Опять же, я хочу подчеркнуть, что сравнение производительности решателя на этих двух разных логиках ошибочно, поскольку они совершенно разные звери, но, надеюсь, вышеприведенные пункты иллюстрируют, почему с плавающей запятой сложно на практике.
AОтличная статья о том, как обрабатывать поплавки IEEE754 в решателях SMT: http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf. Вы можете увидеть множество поддерживаемых операций и почувствовать их сложность.