Формулы Хорна: жадность, которая ставит истину только вынужденно

Если ты знаешь, почему жадное «истина только вынужденно» решает формулы Хорна и почему нарушенный запрет означает отсутствие решения, листай до «Теперь сам».

Как думаешь, когда «поставить ложь» безопасно

Система прав доступа: «администратор может всё», «кто может писать, может и читать», «кто читает бухгалтерию и пишет в кадры - тот видит зарплаты». И запрет: «стажёр не видит зарплат». Вопрос: можно ли выдать права так, чтобы все правила соблюдались и запрет не нарушился?

Прежде чем читать дальше, ответь себе: если переменную никакое правило не заставляет быть истинной, разумно ли оставить её ложной? Может ли истина там, где её не требовали, ПОМОЧЬ выполнить запрет?

На что это похоже

Сборка проекта по зависимостям. Сборщик не собирает модули «на всякий случай» - только те, что нужны: собран a, собран b, значит, можно и нужно собрать c. Когда собирать больше нечего, проверяют запреты вроде «не должно быть одновременно двух версий библиотеки». Если запрет нарушен тем, что собиралось ВЫНУЖДЕННО, никакой другой порядок сборки его не спасёт: те же модули всё равно пришлось бы собрать.

Механизм: вынужденная истина и проверка запретов

правило:  посылки ⇒ вывод      (посылок может быть ноль - это факт)
запрет:   не все из {x, y, …} истинны одновременно

все переменные ложны; очередь = выводы фактов
для каждого правила: счётчик ещё не истинных посылок
пока очередь не пуста:
    x = из очереди; если x уже истинна - пропустить
    x = истина
    в каждом правиле, где x - посылка: счётчик − 1
        счётчик стал 0 → вывод правила в очередь
запрет, у которого все переменные истинны → решения НЕТ
иначе: текущее назначение - решение

Почему верно. Инвариант: каждая переменная, ставшая истинной, истинна в ЛЮБОМ назначении, выполняющем все правила. Для фактов это очевидно. Если правило сработало, все его посылки уже были вынуждены - значит, в любом подходящем назначении они истинны, и вывод тоже обязан быть истинным.

Отсюда оба исхода. Если запрет нарушен - он нарушен переменными, которые истинны в любом решении, значит, решения нет. Если запреты целы - найденное назначение выполняет и правила (каждое правило со всеми истинными посылками сработало) и запреты. Найденное решение ещё и наименьшее: в нём истинно только то, что истинно во всех решениях.

Это обменный аргумент в другой одежде: любое решение можно «уменьшить» до жадного, не нарушив ничего, - лишняя истина правилам не нужна, а запретам только вредит.

Правило

Формула Хорна - правила «все посылки ⇒ вывод» и запреты «не все сразу». Жадный алгоритм ставит истину только вынужденно: начиная с фактов, срабатывает каждое правило, все посылки которого уже истинны. Каждая вынужденная истина истинна во всяком решении, поэтому нарушенный запрет означает, что решений нет, а целые запреты - что найдено наименьшее решение. Со счётчиками посылок - линейное время.

Разбор: права и запрет

правила:   ⇒ a        a ⇒ b        a, b ⇒ c        c, d ⇒ e
запрет:    не (c и e)

очередь [a]:  a истинна → в «a ⇒ b» счётчик 0 → b в очередь;
              в «a, b ⇒ c» счётчик 1
b истинна  →  «a, b ⇒ c» счётчик 0 → c в очередь
c истинна  →  «c, d ⇒ e» счётчик 1 (d ложна) - ждёт
очередь пуста. Истинны a, b, c; ложны d, e
запрет «не (c и e)»: e ложна - цел → решение найдено

добавим правило  b ⇒ d:
    теперь d вынуждена, «c, d ⇒ e» срабатывает, e истинна
    запрет «не (c и e)» нарушен → решения нет ни одного

Во втором случае не помогает никакая перестановка: a - факт, b, c, d, e по цепочке вынуждены в любом решении, а запрет их вместе не допускает.

Разбор: проверка перебором и большой набор

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

import itertools
import random


def horn(n, pravila, zaprety):        # правило: (посылки, вывод)
    istina = [False] * n              # запрет: «не все сразу»
    ostalos = [len(p) for p, _ in pravila]
    gde = [[] for _ in range(n)]      # в каких правилах x - посылка
    for i, (p, _) in enumerate(pravila):
        for x in p:
            gde[x].append(i)
    och = [z for p, z in pravila if not p]       # факты: «⇒ z»
    shagi = 0
    while och:                        # ставим истину ТОЛЬКО вынужденно
        x = och.pop()
        if istina[x]:
            continue
        istina[x] = True
        for i in gde[x]:
            shagi += 1
            ostalos[i] -= 1
            if ostalos[i] == 0:       # все посылки истинны - вывод тоже
                och.append(pravila[i][1])
    if any(all(istina[x] for x in z) for z in zaprety):
        return None, shagi            # запрет нарушен вынужденно
    return istina, shagi


def perebor(n, pravila, zaprety):
    for nabor in itertools.product((False, True), repeat=n):
        if all(nabor[z] or not all(nabor[x] for x in p)
               for p, z in pravila) and \
           not any(all(nabor[x] for x in z) for z in zaprety):
            return True
    return False


rng = random.Random(23)
vyp = nevyp = 0
for _ in range(400):
    n = 12
    pravila = [(rng.sample(range(n), rng.randint(0, 2)),
                rng.randrange(n)) for _ in range(14)]
    zaprety = [rng.sample(range(n), rng.randint(1, 3))
               for _ in range(3)]
    otvet, _ = horn(n, pravila, zaprety)
    assert (otvet is not None) == perebor(n, pravila, zaprety)
    if otvet is None:
        nevyp += 1
    else:
        vyp += 1
        assert all(otvet[z] or not all(otvet[x] for x in p)
                   for p, z in pravila)
print("400 наборов правил: выполнимых", vyp, " невыполнимых", nevyp,
      "- перебор согласен")

n = 100000                            # большой набор: работа линейна
pravila = [(rng.sample(range(n), rng.choice((1, 1, 2))),
            rng.randrange(n)) for _ in range(200000)]
pravila += [([], x) for x in range(20)]
dlina = sum(len(p) for p, _ in pravila)
istina, shagi = horn(n, pravila, [])
print("200 000 правил: истинных", sum(istina), " шагов", shagi,
      " сумма длин посылок", dlina)

400 наборов правил: выполнимых 170  невыполнимых 230 - перебор согласен
200 000 правил: истинных 73965  шагов 196537  сумма длин посылок 266266

Все четыреста ответов совпали с перебором. На двухстах тысячах правил алгоритм сделал меньше шагов, чем сумма длин посылок: каждая посылка уменьшает свой счётчик не больше одного раза, когда её переменная становится истинной. Перебор здесь означал бы 2^100000 назначений.

Что ломается без этого

Первая ошибка - применить тот же приём к правилам с «или» в выводе («если a, то b или c»): это уже не формула Хорна, вынужденной истины нет, и жадность может ошибиться - общая задача выполнимости трудна. Вторая - ставить истину «на всякий случай»: лишняя истина может включить запрет, и алгоритм ответит «нельзя», хотя решение есть. Третья - на каждом шаге перепроверять все правила: на двухстах тысячах правил это квадрат; счётчики посылок дают линию. Четвёртая - проверять запреты по ходу и откатываться: откатывать нечего - всё, что стало истинным, было вынуждено.

Зачем это в работе

Формулы Хорна - это логика правил: системы прав доступа, выводы в экспертных системах и языке Datalog, проверка типов, анализ достижимости в компиляторах, зависимости пакетов без альтернатив. Везде, где правило имеет вид «если всё это, то вот это», ответ на «что следует» и «нет ли противоречия» даёт ровно этот жадный проход - прямой вывод. Знание того, что ровно одно «или» в выводе превращает задачу в трудную, помогает вовремя остановиться и не обещать линейный алгоритм для правил с альтернативами.

Теперь сам

Правила: ⇒ p, p ⇒ q, q, r ⇒ s, s ⇒ p. Запреты: не (q и r), не (p и s). Есть ли решение? Каким будет наименьшее?