Discreet and not discrete.

Обобщённое усиление выведенных из конфликтов ограничений - показывает, что отыскание ограничения конфликта минимального размера является, само по себе, NP-трудной задачей (то есть, даже проверка является NP-полной задачей).

Небольшое пояснение.

Для КНФ (коньюнктивной нормальной формы, то есть, Логического ИЛИ от Логических И от литералов) произвольное присваивание части переменных, совмещённое с выводом значений других переменных, может привести к противоречию. Обычно противоречие выглядит, как вывод одновременно значений истинно и ложно для какой-то переменной: при x=Истина (~x\/y)/\(~x\/~y) выводит и y=Истина и y=Ложь. Разрешение по переменной, для которой обнаружено противоречие, позволяет вывести новое ограничение, которое предотвратит вывод того же противоречия. Процесс разрешения это создание нового ограничения Логического ИЛИ, в которое входят все литералы ограничений, приведших к конфликту, но без литералов переменной конфликта: в нашем примере это, сперва, объединение ограничений (~x\/y\/~x\/~y), из которого исключили повторы и переменную y в любой полярности, то есть, (~x).

Выше продемонстрирован процесс "первого или ближайшего среза" - добавляем ограничение, что наиболее близко к конфликту. Мы можем идти по ациклическому графу вывода к нашему присваиванию, разрешая по любой переменной. В процессе мы можем вывести более короткое ограничение - чем короче ограничение, тем оно сильнее ограничивает пространство поиска.

Статья выше показывает, что поиск наиболее короткого ограничения это NP-сложная задача.

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

Теперь у меня вопрос: какого хрена?

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

https://lex-kravetski.livejournal.com/658115.html (из комментария)

"Критика капитализма в творчестве при господстве капитализма это как Ламборджини в деревне" и далее по тексту мема про Хаскель.

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

Это не означает, что кто-то будет что-то менять, прочитав критику, это важно. Он просто будет чувствовать себя по другому. Как с пресловутым Ламборджини выше.

Отличие от СССР, как я понимаю, в разнице между 1/6 суши (и 1/20 населения) и 5/6 суши и 19/20 населения. Действия внутри СССР по изменению порядка в СССР были бы поддержаны 19/20 населения Земли. А изменения внутри США будут поддержаны кем?.. Даже Китай это всего лишь пятая часть населения Земли.

Дерево слияний в git представляет собой граф, который эквивалентен графу зависимостей возможностей ПО.

Например, если мы сливаем ветки сложный-функционал и тесты-сложного-функционала, и при этом у нас робот проверяет сборку и тесты, то, фактически, в процессе доведения слияния до приемлемого состояния мы выполняем 1) работу по созданию функционала, 2) работу по проверке функционала и 3) работу по отслеживанию требований - нам нужен сложный функционал и нам нужны тесты к нему, чтобы формально его проверить.

Получается, что управление требованиями и планирование можно вести в ветках git/mercurial.

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

Это приводит к простой возможности разделить данные на несколько машин, а также к возможности использовать разные эффективные алгоритмы работы с матрицами, включая оптимизированные алгоритмы умножения матриц (см. hypersparse matrix multiplication и SUMMA).

Здесь мы подходим к необходимости распознавать алгоритмы, записанные пользователем в DSL на циклах, допустим. Ну, это уже было украдено до нас, неоднократно.

Вся индустрия ПО о-ши-ба-ет-ся, особенно, та часть которая "я _________ (датасайнтист/доктор/инженер/финансист - подчеркнуть или вписать), а не программист". Как я уже рассказывал, Amgen обратился в ParSci за решением задачи корректности анализа статистических данных - треть медицинских статей содержала ошибки типа "у эксперимента 1 p=0.04, у эксперимента 2 p=0.038, поэтому мы считаем доказанной гипотезу эксперимента 2" (прямое сравнение p-значений). По идее, отрубив возможность сравнивать p значения напрямую (нет реализации Ord), мы, типами, ограничивали бы возможность допущения ошибок такого типа, получая из Хаскельного кода структуру анализа эксперимента и получения выводов. Они заказали у ParSci библиотеку подключения к R, для использования уже отлаженных и оптимизированных алгоритмов с улучшенными типами, но, как известно, работа ушла на сторону и появился Tweag (если я правильно понимаю).

В дни моего использования Data.IntMap он не был завязан на конкретное представление целого, как ключа. Поэтому его можно было перепилить под меньшее целое (например, 32 бита) и это радикально увеличивало производительность - и мусора меньше, и с кешем получше и, если это кто ещё не знал, 64-битная платформа лучше работает с 32-битными значениями. Поэтому разреженные матрицы связности я хранил в IntMap (IntMap a), что, в сумме позволило обогнать код на Си (clustering coefficients) в десять (10) раз по скорости.

Почему так?

Потому, что IntMap уже сортированные. И их пересечение имеет сложность O(n). При анализе безмасштабных графов вы в обязательном порядке зайдёте на узел со связностью O(количество узлов графа) - так уж устроены эти графы.

Код на Си использовал несортированное представление связности узла - он сперва копировал в буфер, потом сортировал и после выполнял пересечение для сортированных представлений. То есть, при старте с пустого графа выполнялось O(N) сортировок сложностью O(NlogN) для пересечений и O(N) вставок. В сумме сложность была O(N^2logN). При использовании сортированного представления на IntMap мы получаем O(NlogN) сложность вставок и O(N^2) сложность пересечений. Разница на графе в 16 миллионов узлов получилась в десять раз - то есть, код на Хаскеле был медленный (должно было получиться 24 раза), но всё равно быстрее Си.

Что самое приятное, я всё это проделал "не приходя в сознание" - взял сперва Data.Map, потом Data.IntMap, потом поменял ключ в IntMap и вуаля! получил довольно быстро работающую программу.

Вот, вроде, и всё.

PS
История с Tweag уточняется. Может быть, я неправильно помню.

Оригинал взят у vikond65 в Первый Армагеддон

Verilog это 1985 год, на два года позже VHDL, который был основан на языке Ada, принятом в 1979 году.

Для понимания - 1978 это год появления алгоритма вывода типов Хиндли-Милнера, когда в его имени появилось второе имя (первое - это 1968 год). Ada появилась через год после появления ML.

Поэтому Ada имеет структурную систему типов (positive это подмножество integer, или unsigned это такой специально ограниченный std_logic_vector (массив)).

Verilog пошёл по ещё более простому пути - он ВСЁ ЗАШИЛ В ЯЗЫК.

В VHDL есть тип std_logic, состоящий из девяти значений - неопределенного, не подключенного, 1 (буквально - подключение к цепи питания), 0 (подключение к земле), короткое замыкание (соединили вместе 1 и 0), питание через сопротивление, земля через сопротивление, среднее напряжение (как если бы мы смотрели на точку, подсоединённую к питанию и земле через резисторы) и "наплевать" (don't care).

Этот перечисляемый тип позволяет имитировать подключение двух (и более) выходов к одному входу. Таким образом, можно имитировать поведение многофункциональной периферии типа портов ввода-вывода микроконтроллеров.

При желании, в VHDL вы можете создавать свои типы со своими функциями разрешения, например, имитируя протокол самосинхронной логики.

В Верилоге это невозможно.

Не все типы VHDL позволяют соединять два выхода. Например, тип bit (ограничение character: только '0' и '1') так поступать не позволяет. И современная внутрикристальная микроэлектроника тоже не позволяет. Поэтому вы можете написать ядро процессора с использованием bit, bit_vector и соответствующих операций, а периферию описать с помощью std_logic(_vector).

В Верилоге это невозможно. ;)

Вышеуказанное разделение очень важно - положительно, вся современная периферия является аналоговой. Поэтому правильным решением было бы разрешить логику типа bit/bit_vector и периферию моделировать аналогово. Но в во времена создания этих языков на такое не хватило бы всех вычислительных ресурсов мира, поэтому - std_logic и тому подобное.

И если посмотреть на эти языки внимательней, вы поймёте, что такая беда не из-за злого умысла, и не потому, что авторы стандартов не пишут компиляторы. Это потому, что в то время создатели языков не знали и не могли лучшего. При этом создатели VHDL знали чуть лучшее, чем создатели Верилога, которые вообще ленивые сволочи.

А далее изначальные решения проекта языка диктуют направление последующих решений.

Поэтому создавая язык в настоящее время, попробуйте знать лучше, чем средний программист. Как минимум, мне легче будет. ;)

Оригинал взят у jim_garrison в Кто не скачет - Пиночет

https://ru.wikipedia.org/wiki/%D0%92%D0%B5%D0%BB%D1%82%D0%B8%D1%81%D1%82%D0%BE%D0%B2,_%D0%95%D0%B2%D0%B3%D0%B5%D0%BD%D0%B8%D0%B9_%D0%A1%D0%B5%D1%80%D0%B0%D1%84%D0%B8%D0%BC%D0%BE%D0%B2%D0%B8%D1%87

"роман «Ноктюрн пустоты» (1988), описывающий заговор империалистов, угрожающих человечеству климатической войной".

Велтистов гениален, по-моему.

Немного терминологии.

Любую формулу можно привести к коньюнктивной нормальной форме - конъюнкции дизъюнкций литералов. Конъюнкция - Логическое И. Дизъюнкция - Логическое ИЛИ. Литерал здесь - прямое или обратное значение булевой переменной. x или ~x. Дизъюнкцию ещё можно называть ограничением, именно они ограничивают возможные значения переменных КНФ.

Самый первый алгоритм вычисления выполнимости (Davis-Putnam, DP) делал так называемое разрешение (resolution): если у нас есть в КНФ две дизъюнкции x\/Y и ~x\/Z, то мы можем заменить две эти формулы на формулу y\/z. Здесь x переменная, а Z и Y - дизъюнкции. Алгоритмически это выполняется так: для всех a, содержащих x и всех b, содержащих ~x, выполнить разрешение a и b. Исходные формулы можно убрать. Если разрешение выполнялось для формул вида x\/y\/A и ~x\/~y\/B, то в результате получится тривиальная формула y\/~y\/A\/B - тождественно равная истине.

Если при итеративном применении этого правила мы пришли к пустой дизъюнкции, то формула невыполнима (пример: x/\~x). Если в конце получилась пустая формула (все разрешения завершились тривиально), то формула выполнима. Может также получиться набор независимых формул, в этом случае тоже легко найти решение. Если мы не можем произвести разрешение по какому-то литералу, то по нему нельзя сделать выбор - зафиксируем его переменную в его значении.

Этот вариант требует большого количества пространства.

Второй алгоритм, предложенный Logemann и Loveland (LL в сокращении DPLL), перебирал значения всех переменных КНФ. Зафиксировав значение переменной, он проверял, не выводятся ли значения других переменных из уже зафиксированных и не приводит ли этот вывод к противоречию. Если можно было произвести вывод значений, он производился. Если у нас вывелись два противоположных значения, то это противоречие. При противоречии производился откат, убирались все результаты текущего вывода и фиксированное значение заменялось на противоположное.

Вот простая КНФ: a \/ b \/ c /\ a \/ b \/ c. Если мы зафиксируем значения a=Ложь и b=Ложь, то из первой дизъюнкции выводится c=Истина, а из второй - c=Ложь. Противоречие. Заменив любое из фиксированных значений a и b, мы получим удовлетворяющее присваивание.

Зайдем с другой стороны. Зафиксируем c=False. Вторая дизъюнкция станет тривиально истинной. Останется только первая. Выберем a=Ложь, останется только вывод b=Истина.

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

Это очень важно. Решатель Minisat показывает отличные результаты в категории "Индустриальные задачи" в соревновании решателей булевой выполнимости в частности потому, что он выбирает для новых переменных значение v=Ложь. Оказывается, большая часть задач этой категории имеет решение с ключевыми переменными, равными Лжи. А вот в категории "Случайные задачи" он отстает - там отлично работают системы, что учитывают структуру задачи (решатель march_xx из таких, например) или просто стохастические алгоритмы типа WalkSAT.

В середине 90-х решатель GRASP совершил прорыв - он начал запоминать причины, по которым решатель пришёл к конфликту, добавляя дизъюнкции противоречия (conflict clauses) к задаче. Здесь преследуются две цели - избегнуть в будущем похожей ситуации и автоматически перещелкнуть последнее выбранное значение.

Пример приведу все на том же конфликте выше. Мы установили переменные a=Ложь и b=Ложь и получили конфликт c и ~c. Мы говорим, что мы не должны посетить в будущем такой набор переменных, при котором a=Ложь И b=Ложь. Мы добавляем к нашей задаче ещё одно ограничение - ~(~a/\~b)=a\/b. Последней мы выбрали переменную b, отменяем её выбор. Новая задача a\/b\/c /\ a\/b\/~c /\ a\/b с выбором a=Ложь автоматически выберет b=Истина (третье ограничение) и решение будет найдено.

Это риешение важно ещё и потому, что если мы запоминаем все причины конфликтов, то мы (а) экспоненциально быстрее полного перебора (доказано) и (б) можем начинать с чистого листа и не придём к той же ситуации.

Рестарт перебора с чистого листа позволяет избежать перебора в окрестности заведомо плохого решения.

Современные решатели начинают с чистого листа довольно часто - после нескольких сотен конфликтов. Есть тендениця ещё увеличить частоту рестартов.

Надо далее рассказать про способы выбора ограничений противоречий, а также надо рассказать про реальную реализацию перебора в том же MiniSAT.

Последняя ссылка на сегодня - glueminisat. Это вариант всё того же MiniSAT, только с улучшенным механизмом выбора ограничений противоречий.

LISP 1.6.

Тот самый. IBM-овский. От МакКарти.