https://scholarspace.manoa.hawaii.edu/server/api/core/bitstreams/8e872576-b70c-457d-a458-d260f21d66f3/contentRead more... )

http://essay.utwente.nl/91688/1/Tomov_BA_EEMCS.pdf - здесь товарищ пытается собирать "графы Логических И с Отрицаниями" (and-inverter graph) для логических схем, представленных в виде ROBDD.

Использует он алгоритм, что позволяет получить неупрощаемые примитивные ( Read more... )

https://arxiv.org/pdf/cond-mat/0408190.pdfRead more... )

Начало про общую идею, необходимые структуры данных и тп ( Read more... )

Я тут в твиттере распространялся про поиск наикратчайшего ограничения при поиске решения в алгоритме выведения ограничений из конфликтов (решение задачи логической разрешимости).

Важно найти наикратчайшее ограничение. "Сила" ограничения пропорциональна 2-длина ограниченияПри поиске ограничений мы 1) имеем дело с множеством "нарезаний" фронтов ( Read more... )

http://www.scientificamerican.com/article/rational-and-irrational-thought-the-thinking-that-iq-tests-miss/Read more... )

http://www.cs.bgu.ac.il/~mcodish/Papers/Sources/lopstr07.pdf

SAT был использован для проверки завершимости набора правил переписывания. Кодирование проблемы в CNF и запуск Minisat быстрее в сотни раз, чем специализированное решение.

Minisat ещё и не самый

Немного терминологии ( Read more... )

Поскольку у меня последнее время идиосинкразия к большим постам, буду конспективно ( Read more... )

Тут zelych занимается решением логических уравнений. Он сделал преобразования Цейтина, и из таблички умеренного размера (100К строк с ограничениями) получил очень большую КНФ в полтора миллиона дизъюнктов.

По идее, можно справиться лучше.

Сперва код:
import Data.Bits ( Read more... )