TL;DR
- Расширение Шеннона - это формула для разложения булевой функции в один MUX.
- Кофактор - это "новая функция, которая фиксирует одну переменную в 0/1", так что эта переменная исчезает внутри кофактора.
- Булева разница - это функция чувствительности, которая вычисляет "изменится ли выход, если перевернуть вход x?".
- ∃(экзистенциальное) квантование - это формула "должно существовать только одно решение", которая является ядром SAT.
- Почему оптимизация трудна: SAT - это поиск одного решения, оптимизация - это сравнение всех кандидатов.
1. Проблема: когда карта Карнауха ломается
1.1 40 переменных, карта Карнауха заканчивается
- 2^40 шкала → "Я могу это нарисовать, но не могу написать"
- Вывод: мы должны рассматривать булевы функции как структуру данных + оператор, а не руку.
1.2 3 вещи, о которых эта статья
- декомпозиция (разложение)
- вычисление (представление, с которым может работать программа)
- применение (простая операция в EDA)
2. Кофактор Шеннона: новая функция, созданная путем "исправления переменной"
2.1 Определение: Кофактор - это подстановка
- Для входной переменной x в f, a
- положительный кофактор: ( f_{x} = f(x=1) )
- отрицательный кофактор: ( f_{~{x}} = f(x=0) )
2.2 Ключевой момент: "Это новая функция, x исчезает"
- Мы исправили x на 0/1, поэтому x больше не может появиться в результате.
- Если вы упустите это, все последующие булевы разности/количества развалятся.
2.3 (краткий пример)
- Пример: ( f(x,y,z) = xy+x~z+~xyz )
- ( f(x=1) = y + \bar{z} ) (можно упростить)
- ( f(x=0) = yz )
3. Расширение Шеннона: "Булева функция = MUX"
3.Теорема 1 (теорема расширения Шеннона)
Для любого f и любой переменной x:
f=x⋅f(x=1)+~x⋅f(x=0)
3.2 Аппаратная перспектива: расширение Шеннона = 2:1 MUX
- select = x
- data1 = f(x=1)
- data0 = f(x=0)
- output is f
📌 Вот здесь и появляется смысл "ветвления":
- Когда мы идем по ветви x=0, нам нужно смотреть только на f(x=0)
- Когда мы идем по ветви x=1, нам нужно смотреть только на f(x=1)
3.3 MUX-дерево = рекурсивная декомпозиция
- 1 переменная → 2 ветви
- 2 переменные → 4 ветви
- k переменных → 2^k ветвей
- Это выглядит как "перечисление", но EDA делает здесь обрезку. (объяснение последует позже)
[Рисунок 1] Расширение Шеннона с 2:1 MUX
[Рисунок 2] Иллюстрация дерева MUX, в котором расширение с двумя переменными создает четыре листа
4. Кофактор означает "обмен операциями": 계산이 쉬워지는 이유
4.1 Очень важное свойство
- комплимента:
- (~f)x=~(𝑓𝑥)
- AND/OR/XOR также позволяет "сначала кофактор → потом операция"
- (𝑓∧𝑔)𝑥=𝑓𝑥∧𝑔𝑥
Иными словами, вы не составляете большое выражение, а затем его кофактор, а
сначала кофактор, чтобы сделать выражение меньше, а затем вычислить его.
5. Булева разница: "чувствительность" как формула
5.1 Определение
∂f/∂x=f(x=1)⊕f(x=0)
5.2 Значение: "Условие, при котором выход изменяется при переключении x"
- XOR - это "1, если отличается"
- Таким образом, на входном шаблоне с булевой разницей 1:
- Если x меняется с 0→1 или 1→0, то f должен измениться
5.3 Чувствительность на примере
- инвертор: f=~x
- 𝑓(1)=0,𝑓(0)=1⇒∂𝑓/∂𝑥=1
- Всегда чувствителен
- AND: ( f=xy )
- 𝑓(1)=𝑦,𝑓(0)=0⇒∂𝑓/∂𝑥=𝑦
- Изменение x влияет на выход только при y=1
- OR: ( f=x+y )
- 𝑓(1)=1, 𝑓(0)=𝑦 ⇒ ∂𝑓/∂𝑥=~𝑦
- воздействует только при y=0
5.4 Правильная интерпретация фразы "x не оказывает логического влияния на F?"
- Не означает "всегда не оказывает".
- Означает, что при определенных условиях ввода он может не иметь эффекта.
- Выбор этих условий и есть булева разница.
[Рисунок 3] Иллюстрация того, почему булева разность становится y / ȳ в И/ИЛИ
6. Квантификация: “변수 제거”를 목적 함수로 만든 연산
6.1 экзистенциальная квантификация (∃): "требуется только одно решение"
∃xf=f(x=0)∨f(x=1)
- Смысл: при фиксированных прочих исходных данных хороший выбор x приводит к f=1?
6.2 универсальная квантификация (∀): "должно быть истинным во всех случаях"
∀xf=f(x=0)∧f(x=1)
- Смысл: всегда ли f=1 истинно, независимо от того, каков x?
6.3 соответствия 1:1 с предложением, которое вы сказали
"Вам не нужно перечислять их все, вы просто должны найти любой один год"
Вот именно это вы и сделали:
∃ квантификация
- А основная форма SAT:∃X:F(X)=1
7. SAT против оптимизации: почему "оптимизация" жестче
7.1 SAT - это "найди один и готово"
- Заканчивается, когда существует решение, удовлетворяющее условию
- Может быть прервано (обрезка)
7.2 Оптимизация - "сравнение - это суть"
- Чтобы доказать, что существует лучшее решение
- нужно продолжать рассматривать другие ветви
- Поэтому оптимизация EDA структурно трудна (что приводит к NP-трудной истории)
[Рисунок 4] SAT останавливается на первом удовлетворении, Optimisation keeps exploring
다음 강의로 자연스럽게 연결: Tautology와 URP
8.1 Является ли тавтология "всегда 1?"
- f≡1?
- Ключевая идея: если f - тавтология, то ⇔ f(x=0) и f(x=1) - обе тавтологии
8.2 Интуиция URP
- Разложение на кофакторы Шеннона (ветвление)
- Окончание прямо посередине (сильное обрезание)
- В итоге получается не алгоритм "перечисления", а алгоритм "отбрось то, что можешь быстро"
이 글에서 반드시 가져가야 하는 5개
- cofactor는 substitution이며, В полученной функции переменная исчезает
- Расширение Шеннона является одновременно формулой и 2:1 MUX-модель
- Булевая разность - это функция, которая дает "условия, при которых изменение x влияет на выход"
- ∃ квантификация реализует "нужен только один" как ИЛИ
- SAT - это один и готово, оптимизация занимает больше времени из-за сравнений
.