Разработка алгоритма для поиска совпадений таблиц истинности

Воробьев Алексей Михайлович

Руководитель: Куликов Александр Сергеевич

Разработка Программного Обеспечения

Университет ИТМО

2024

Актуальность

/22

2

Логический синтез – процесс получения наиболее оптимальной логической формулы по заданной таблице истинности. Наиболее часто данная задача встречается в цифровой электронике.

Таблицы истинности

/22

3

Таблица истинности (2 входа и 2 выхода)

Трансформации

/22

4

Результирующая таблица истинности

Исходная таблица истинности

Трансформация таблицы

Актуальность

/22

5

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

Конференция IWLS

IWLS – это международная конференция по логическому синтезу.

Наша команда в данный момент участвует в соревновании.

Надо найти оптимальные формулы для 100 таблиц.

/22

6

Таблицы соревнования имеют количество переменных от 6 до 16.

​

• Таблицы соревнования можно использовать для проверки алгоритма
• Благодаря алгоритму можно будет получить логические формулы

Анализ существующих решений

/22

7

• The Art Of Computer Programming [1]
• обрабатываются только таблицы с небольшим количеством переменных n ≤ 6
• Large-Scale Boolean Matching [2]
• обрабатываются формулы, а не таблицы истинности
• не обрабатываются инвертирования, только перестановки

1. https://cs.stanford.edu/~knuth/taocp.html
2. https://www.researchgate.net/publication/221339893_Large-Scale_Boolean_Matching

Цель: реализовать эффективный алгоритм для поиска совпадений таблиц истинности и генерации оптимальных логических формул.

Задачи:

• Придумать и реализовать эффективный алгоритм для поиска совпадений
• Написать скрипт для генерации формул в соответствии с найденной трансформацией
• Сгенерировать 100 оптимальных формул для таблиц соревнования

/22

8

Фиктивные входы и выходы

/22

9

Используемые переменные

00001111

10101010

100 01

001 10

Сокращённая таблица истинности

Тривиальные подходы

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

/22

10

Полезные наблюдения

• При перестановках и инвертированиях входов количество единиц в строке таблицы (выход) не меняется
• При инвертировании выхода 0 и 1 в строке меняются местами
• По количеству единиц можно определить мог ли один выход преобразоваться в другой, а также определить инвертирование выхода

/22

11

Идея алгоритма

Для каждой переменной определим набор:

/22

12

Идея алгоритма

При инвертировании входа инвертируется первый индекс:

/22

13

При инвертировании выхода инвертируется второй индекс:

Данные наборы сохраняются (с точностью до инвертирований) при перестановках и инвертированиях переменных, с помощью этого можно упростить перебор.

Поиск общей трансформации

Каждый выход может иметь много трансформаций, нам надо найти общую трансформацию.

/22

14

Трансформации конфликтуют:

Трансформации не конфликтуют:

Общая трансформация:

Преобразование множеств трансформаций:

A – таблицы с малым числом трансформаций для каждого выхода.

B – таблицы с большим числом трансформаций для выходов и большим числом конфликтов.

С – таблицы с большим числом трансформаций для выходов и малым числом конфликтов.

D – таблицы с одним выходом.

/22

15

Ограничение по времени ≈ сутки

Маски

/22

16

Маски

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

/22

17

Перестановка выходов

/22

18

Анализ не обработанных таблиц пролил свет на такой случай:

Перестановка выходов

/22

19

Сделаем перестановку выходов:

Перестановка выходов

Для того, чтобы обработать последнюю таблицу, я воспользовался информацией о её структуре.

/22

20

Скрипт для генерации формул (BENCH)

BENCH файл

/22

21

INPUT(x0)

INPUT(x1)

x0_inv = NOT(x0)

y0 = AND(x0_inv, x1)

y1 = OR(x0_inv, y0)

OUTPUT(y0)

OUTPUT(y1)

INPUT(x1_inv)

x1 = NOT(x1_inv)

INPUT(x0)

x0_inv = NOT(x0)

y0 = AND(x0_inv, x1)

y1 = OR(x0_inv, y1)

OUTPUT(y0)

y1_inv = NOT(y1)

OUTPUT(y1_inv)

Новый BENCH файл:

Результаты

• Было реализовано семейство эффективных алгоритмов для поиска совпадений таблиц истинности
• Был реализован скрипт для генерации формул по заданной трансформации
• Были сгенерированы 100 оптимальных формул для таблиц из соревнования

​

/22

22

Исходный код:

https://github.com/PinochetLab/truth-table-match-find-algorithm

​

Вопрос №2

Когда алгоритм находит возможную трансформацию, запускается функция, которая проходит по строкам и сравнивает их посимвольно.

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

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

/22

23

Вопрос №2

Идея была проверена на одной из таблиц

/22

24

Последняя таблица

Последняя таблица представляет собой худший случай алгоритма поиска подстановок – много одинаковых наборов.

/22

25

Одним цветом указаны наборы, равные с точностью до инвертирований.

Последняя таблица

/22

26

Скрипт для проверки получившихся BENCH файлов

Была использована система ABC (система для синтеза и верификации) для проверки того, что:

• Сгенерированный BENCH файл соответствует таблице истинности
• Сгенерированный BENCH файл не стал больше оригинального (больше не по размеру, по количеству AND узлов)

/22

27