Pull to refresh

Обсуждение работы алгоритма Романова на примере

Algorithms
В продолжение вчерашнего обсуждения.

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

Для дальнейшего обсуждения я написал небольшой unit-тест, который оперирует формулой из примера. Unit-тест нужен для того, чтобы пропустить шаг алгоритма Романова, где происходит декомпозиция исходной формулы на множество CTF. Вместо этого декомпозиция предлагается изначально автором вопроса.

Unit-тест и подробный лог работы приложения я выложил здесь:

gist.github.com/791064

Предлагаю по возможности ссылаться туда по номерам строк (там не совсем удобно, что нельзя дать прямую ссылку на номер строки, придется искать ее вручную; если кто-то предложит более удобный сервис, я перенесу лог туда).

Как видно из лога работы, тест заканчивается ситуацией, когда на очередном шаге построения гиперструктуры базисный граф оказался пустым множеством, что согласно алгоритму означает, что формула не выполнима (пункт 2b внизу страницы 11 в тексте статьи).

Чтобы не переписывать здесь еще раз статью, предлагаю в обсуждении задавать вопросы, которые требуют дополнительных разъяснений.
Tags:алгоритмывычислительная сложностьдоказательствоjavaopen sourcecomputer science
Hubs: Algorithms
Total votes 26: ↑21 and ↓5 +16
Views2.5K

Comments 24

Only those users with full accounts are able to leave comments. Log in, please.

Popular right now

Technical Lead, Open Source
from 8,000 $Cube.jsRemote job
Distributed Systems Engineer
from 8,000 $Cube.jsRemote job
Technical Lead, Cloud Platform
from 8,000 $Cube.jsRemote job
Data Science Cloud Engineer (remote)
from 200,000 to 300,000 ₽Bergmann InfotechRemote job
Java developer
from 150,000 to 300,000 ₽EmphasoftСанкт-Петербург

Top of the last 24 hours