Решения SAT для определения функций многомерных функций?

Question

Boolean Satisfiabiity problem является обобщением для проверки выполнимости булевого выражения. Теперь булево выражение генерируется алгоритмом неотрицательности многочлена. Полином может быть, например, и с некоторым интервалом, таким как , где - это количество переменных. В настоящее время я проверяю особенности многочленов, таких как неотрицательность, с помощью специальных алгоритмов, таких как алгоритм с ветвями и границами, где я делаю большую проблему меньшими задачами, но упускаю такие функции, как обучение, обещанное некоторыми решателями SAT, например MiniSat. Так

1. Некоторых решатели SAT предназначен для проверки свойств многочленов, таких как полилинейные функции или общих функции многих переменных?

2. Любой простой способ преобразования многомерной функции и алгоритма неотрицательности в булево выражение?

Answer 1

После беглого поиска, кажется, не существует каких-либо решателей SAT специально для этой цели или алгоритмы, чтобы сделать преобразование вы упомянули. Таким образом, кажется, что ответ на оба ваших вопроса - «нет».

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

Более подходящей парадигмой будет constraint programming, хотя решатели, поддерживающие непрерывные области, редки.

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