Про насыщение равенствами. Снова.

Jun 07, 2011 23:59

В гугле.

Предыдущие серии.

Напомню кратенько содержание.

Мы берём некоторое выражение и начинаем его преобразовывать в эквивалентные ему. (a+0)=(0+a)=a, a+(b+0)=a+(0+b)=(a+b)+0=(b+a)+0=0+(a+b)=0+(b+a)=a+b=b+a. Если мы создали что-то новое, то мы добавляем его в нашу кучу выражений и пытаемся применить к нему преобразования. Однако может так выйти, что наше выражение уже встречалось, тогда мы не будем проходить по нему заново. Вон, выше a+b и b+a будут разделены сразу между несколькими выражениями. Также не будут создаваться новые узлы для a, b и 0.

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

Что применили авторы подхода? Они применили псевдо-булеву оптимизацию.

Это когда у нас есть, во-первых, целевая функция вида min=ΣaiΠxαij, в которой xαij - "булевы" переменные, то есть, переменные, принимающие значения 0 и 1. αij принимают значения 1..N. Во-вторых, у нас есть ограничения в виде булевой функции на xk, например, КНФ. Целевая функция содержит "стоимость" узлов, а ограничения содержат ограничения на их совместность.

Возьмём выражение a+0. Оно может быть преобразовано в 0+a и a. Итого, узлов у нас будет 4, пометим их переменными x1..4: x1 соответствует 0, x2 соответствует a, x3 - a+0 и x4 - 0+a.

Сперва составим ограничения.

Мы должны выбрать один из узлов x2, x3 или x4 в качестве решения. Это записывается, как дизъюнкция конъюнкций: x2∧~x3∧~x4∨~x2∧x3∧~x4∨~x2∧~x3∧x4.

Если выбраны узлы x3 или x4, то обязаны быть выбраны узлы x1 и x2, без них граф будет не полон: (x3∧x1∧x2∨~x3)∨(x4∧x1∧x2∨~x4). Переводится это так: "если выбран узел со сложением, то должны быть выбраны узлы, от которых он зависит, в противном случае нас не волнует, выбраны ли узлы-операнды".

Эти наши условия должны выполняться одновременно. Поэтому мы объединим их ниже по ∧.

И далее следует целевая функция. Сложение считаем ценой 2, операнд типа константа или переменная - 1. Получится вот, что: min=2x3+2x4+x2+x1.

И перепишем всё полностью:
 (x2∧~x3∧~x4∨~x2∧x3∧~x4∨~x2∧~x3∧x4)
∧(x3∧x1∧x2∨~x3)
∧(x4∧x1∧x2∨~x4)
min=2x3+2x4+x2+x1

Всего решений системы ограничений 4 (в виде вектора x1..4, в скобках значение целевой функции): x1="1110" (5), x2="1101"(5), x3="1100"(2) и x4="0100"(1).

Минимум достигается при x1=0, x2=1, x3=0 и x4=0. x2 у нас соответствовал переменной a.

Наш результат a.

По-моему, изящно.

Всё становится интересней, когда надо выбирать "наиболее широкие" выражения. a+(b+(c+d))=(a+b)+(c+d). Они более "параллельны".Придётся учитывать "путь", вводить промежуточные переменные и тп.

Зачем мне это надо?

Это мне надо для ассемблера узлов моего "вычислителя будущего". Стековый код достаточно плотен, но не удобен для написания программ. Вот для преобразования регистрового кода в стековый мне и нужна такая штука.

Потом я думаю использовать её ещё и в другой части кодогенератора.

вычислитель будущего, sat, генерация кода, оптимизация

Previous post Next post
Up