All streams
Search
Write a publication
Pull to refresh
36
0
Сергей @CaptainTrunky

Научный сотрудник

Send message
Это же типичная задача SAT, разве нет? Перегоняете все свои функции в КНФ форму, добавляете вспомогательные переменные, соответствующие выходам функций, задаете им соответствующие значения, затем запускаете SAT солвер, он вам и найдет какое-то решение, из которого можно будет достать входные значения.
У нас пары могут состоять из разных объектов. К примеру, как элементы паззла — чтобы проверить, подходят ли друг другу кусочки, нужно вот прям взять их и попробовать соединить. Если все сошлось — сохраняем, если нет — идем дальше. Вот только в нашем контексте в итоге оказалось, что можно сгенерировать не отдельные элементы, а сразу все пары, без дальнейших проверок.
Как-то раз возникла задача попарного сравнения некоторых объектов и поиска определенных пар, сложности, соответственно, О(n^2). Т.к. количество объектов было неприлично большим, то решение в лоб работало слишком медленно. Пораскинув мозгами, сделали вывод, что объекты можно не сравнивать после их получения, а построить нужные пары сразу. Казалось бы, задача свелась аж к NP-полной, но на многих кейсах ускорение было с десятков минут до нескольких секунд. Само решение опирается на Boolean SAT. Где б мы были без теоретической подготовки...
А можно вас попросить написать прототип для автоматизации предложенного решения и прогнать его через бенчмарк/другой? Было бы любопытно посмотреть, как конкретно влияет такая минимизация на конечный результат. Ну и да, если сегодня говорить о проблемах минимизации функций, то тут интерес представляют функции куда большей размерности, чем 16 (мое сообщение чуть ниже).

PS
Эх, доделать бы свою версию espresso, оптимизированную под совсем большие задачи...
Я не использовал espresso очень уж активно, исключительно как минимизатор и cnf-2-dnf, dnf-2-cnf транслятор. Если в нем и есть умный алгоритм работать с частичными функциями под опциями, то я не знаю. С другой стороны, ведь написать скрипт, который бы склеил набор нетлистов в один — это дело пары часов, разве нет? Пусть у нас есть большой нетлист, составленный из частичных функций. Каждому входу/выходу соответствует некая переменная в PLA (или BLIF, что там у вас). Теперь начинаем перечилсять известные нам "решения" для этого большого нетлиста (строки в PLA, они же конъюнкты). Неизвестные или несущественные значения переменных заполняем don't care (например, мы точно знаем, что вход одного нетлиста никак не влияет на вход другого). Все, получившийся большой файл можно запихивать в espresso. Если я что-то не так понял или криво объяснил, предлагаю перехать в личные сообщения. )
Да, легко. Espresso сносно работает с функциями до 200 переменных, потом как повезет. Есть опыт использования на функциях как раз с 180+ переменными и несколькими десятками тысяч строк. В мои требования по рантайму (20-30 минут — это норма) вполне укладывается.
Да. Если есть булева формула F (x0, x1, x2), то конкретные значения x0, x1, x2 (истина или ложь) называют интерпретацией. Соответственно, интерпретации могут быть ложжными и истиными (в зависимости от значения F).
Доброй фазы вращения Земли вокруг своей оси!
Я использовал «по-симпатичнее» не только в контексте красочности. Я включил в это понятие удобство пользования и остальные аспекты из статьи.:)
Согласен, система из поста выглядит посимпатичнее. С другой стороны, каких-то существенных проблем в Перекрестке у меня тоже не возникало. Самообслуживание как самообслуживание, да и персонал рядом сидит, чтобы помочь в случае чего.
Подобная система еще в Перекрестке у метро Крылатское.
Только что обновил с F20 KDE-spin. Никаких проблем не возникло, единственное что — fedup установил ВСЕ ПО для Gnome версии Fedora.
Стоит ли обновляться с Fedora 20 или все же велик риск все непоправимо окирпичить? Никаких хитрых драйверов в текущей системе нет, грязные хаки не испытывал. Использую KDE спин в дуал-буте с Win 8.1.
А в каком контексте, если не секрет, понадобилась новая реализация? Какую проблему вы решаете?
Он прошлой зимой посещал Москву. Ему предложили потусить в неформальной обстановке с активной околонаучной молодежью в числе аж 5-6 человек, куда я и затесался. Найджел — невероятно позитивный и веселый человек, который на протяжении часа рассказывал нам всякие всякости о своей жизни и его взгляде на будущее подобных технологий. В один момент отстегнул руку и дал нам с ней поиграться немного. :)
И это, кстати, тоже. Найджел много рассказывал на эту тему.:)
Я обсуждал этот вопрос с Найджелом лично. Его позиция примерно такая: «Сегодня нет заменителей кожи достаточно хорошего качества, все равно заметно, что с рукой что-то не так. При этом сам вид искусственной кожи вызывает своего рода антипатию, отвращение (выглядит как кожное заболевание или что-то подобное). В свою очередь просто протез вызывает куда меньше вопросов и выглядит просто круто, футуристично»
А нельзя ли тут как-то добавить анализ возникших конфликтов? Что-то в духе SAT — conflict-driven clause learning. Запоминать конфликтующие пересечения до достижения некоего лимита по памяти, потом вычищать БД конфликтов.
Тут же пригодится и random restart — если программа застряла в процессе построения, можно попробовать просто начать либо совсем с нуля, но с иными начальными условиями, либо откатиться на большее число итераций.
Я бы еще добавил, что существует Python-интерфейс к PARI/GP в Sage. Очень удобно использовать огромное кол-во библиотек с под более-менее единым интерфейсом.
Добрый день. Существенно изменились жизненные обстоятельства, возникли другие задачи, так что сейчас я не могу уделать этому проекту досточного объема времени. Я вам в течение пары дней постараюсь ответить. если хотите — можно связаться через личку/почту.

Information

Rating
Does not participate
Location
Россия
Date of birth
Registered
Activity