Pull to refresh

Comments 14

Может иметь смысл расширение матрицы с 2D на 3D. Или до размерности соответствующей количеству переменных.
Хм… А как тогда вручную минимизировать в 7-мерном пространстве?
С помощью срезов. Как крестики-нолики 3д на бумаге. Но такую задачу больше не нужно решать руками, у нас же есть специальные роботы!
А нужно ли её минимизировать вручную? В 2016м-то году?
Вопрос из серии — надо ли знать таблицу умножения, если полно калькуляторов?
Давно уже ищу способы решения такой задачки, может кто с хабра подскажет?
Есть кейс: пару сотен булевых функций от примерно 5 сотен переменных. Задача: для заданного вектора результатов найти значения переменных или хотя бы упростить исходную систему для возможности полного перебора. Этакие булевые СЛАУ.
Это же типичная задача SAT, разве нет? Перегоняете все свои функции в КНФ форму, добавляете вспомогательные переменные, соответствующие выходам функций, задаете им соответствующие значения, затем запускаете SAT солвер, он вам и найдет какое-то решение, из которого можно будет достать входные значения.
Как сказал CaptainTrunky, Ваша задача легко укладывается в SAT. Но решение SAT вам позволит найти значения переменных. Что касается минимизации, то тут или аналитически или генерируя все возможные решения SAT задачи (ALL-SAT). Размер результата очень сильно зависит от КНФ, вплоть до невообразимых величин, тут важна информация о самой КНФ: встречаемость литералов в конъюнктах, отношение колиества переменных к количеству конъюнктов и т.п. Касательно ALL-SAT, могу дать пару соображений.
Спасибо, теперь хоть буду знать в какую сторону копать.
До этого начал уже придумывать способы ухода в базис Жегалкина и дальше аналогично методу Гаусса в СЛАУ решать их (хотя проверял только на 3 переменных и трех уравнениях, так что на возможность такого решения для 100+ переменных не ручаюсь). Собственно размеры уравнений в базисе пугает (в пределе 2^n коньюнкций по (1;n) переменных), хоть и очень разряженная матрица получается, а ощущение неправильности способа решения не покидает и почти уже бросил затею, т.к. играюсь для себя.
Можно еще попробовать навести оптимизацию при помощи булевых счетчиков. Задаем дополнительные ограничения на кол-во определенных литералов, после чего инкрементально увеличиваем счетчик от нуля до тех пор, пока не придем к SAT решению. Счетчики тоже могут получиться невообразимо большими, но что поделать. Как и tvi, могу помочь более детально.
Не понятен Ваш способ. Я правильно понимаю что Вы задаете ограничение на количество конъюнктов, в которых будет распространяться приписывание литерала? Но тогда где гарантия, что мы найдем все решения (ведь без них мы не получим минимизации)?
Прошу прощения, я изначально неправильно прочитал постановку задачи. Согласен, AllSAT выглядит самым разумным решением для данной задачи, вопрос только в форме КНФ и кол-ве возможных решений. Я сейчас занимаюсь чем-то похожим. :)
На практике в FPGA все равно булевы функции записываются в LUT (Look-Up Table), это такая ПЗУ-шка на N входов и в ней хранится битовая таблица 2^N.

Минимизировать надо, если из К155ЛА3 собирать логику :)
Но ведь логика не только в FPGA нужна. :)
Мы вот ее в вычислительную геометрию пихаем и нам ох как нужна минимизация.
Sign up to leave a comment.

Articles