С момента предыдущей публикации о полиномиальном алгоритме Романова для 3-ВЫП прошло 4,5 месяца.
За это время мы с Владимиром Федоровичем подготовили вариант статьи, чтобы отправить его коллегам-ученым и попутно реализовали эталонную реализацию этого алгоритма на Java.
За основу статьи мы взяли существующую публикацию на английском языке, на которую я давал ссылку в предыдущем посте. Текущая версия отличается лишь небольшими дополнениями, которые должны, по нашему мнению, упростить понимание алгоритма и приведенных доказательств. По совету kichik статью опубликовали на arXiv.org:
Non-Orthodox Combinatorial Models Based on Discordant Structures
arxiv.org/abs/1011.3944
Сегодня мы составили открытое письмо, которое отправили некоторым ученым, чьи контакты удалось найти (спасибо alexeyrom за ссылки). Письмо также опубликовано на сайте, который мы сделали специально для обсуждения:
3-SAT: Novel Model
romvf.wordpress.com/2011/01/19/open-letter
Если у кого-то есть контакты ученых, которые занимаются этой тематикой, пожалуйста, отправьте им это письмо. Мы будем рады любым отзывам и замечаниям.
По ходу работы над новым вариантом статьи мы разбирались с алгоритмом, чтобы написать эталонную реализацию на Java. У нас получилось! Первую версию приложения мы опубликовали 19 ноября на github под лицензией LGPL version 3:
Reference Implementation of Romanov's Polynomial Algorithm for Boolean 3-SAT Problem
github.com/anjlab/sat3
Сейчас это однопоточная реализация, представляющая собой консольное приложение, которое читает формулы из файлов формата DIMACS CNF и выдает на выходе выполняющий набор если формула выполнима, или выдает соответствующее сообщение, если формула не выполнима. Программа ведет подробный лог, который должен помочь читателям статьи разобраться в работе алгоритма.
Для затравки, вот базисный граф с выполняющим набором для примера из статьи (слева) и для формулы с количеством переменных равным 100 (справа, кликабельно):
Подробнее описание результатов работы приложения можно найти здесь. Там же на github есть readme и несколько страничек в wiki с пояснениями как запустить приложение.
Последняя опубликованная версия — 1.0.3. Но в HEAD лежат несколько дополнительных оптимизаций, которые ускоряют работу приложения в 2 раза (версия 2.0.0-SNAPSHOT).
Дальнейшая работа может быть разделена на несколько направлений.
За это время мы с Владимиром Федоровичем подготовили вариант статьи, чтобы отправить его коллегам-ученым и попутно реализовали эталонную реализацию этого алгоритма на Java.
Статья и открытое письмо ученым
За основу статьи мы взяли существующую публикацию на английском языке, на которую я давал ссылку в предыдущем посте. Текущая версия отличается лишь небольшими дополнениями, которые должны, по нашему мнению, упростить понимание алгоритма и приведенных доказательств. По совету kichik статью опубликовали на arXiv.org:
Non-Orthodox Combinatorial Models Based on Discordant Structures
arxiv.org/abs/1011.3944
Сегодня мы составили открытое письмо, которое отправили некоторым ученым, чьи контакты удалось найти (спасибо alexeyrom за ссылки). Письмо также опубликовано на сайте, который мы сделали специально для обсуждения:
3-SAT: Novel Model
romvf.wordpress.com/2011/01/19/open-letter
Если у кого-то есть контакты ученых, которые занимаются этой тематикой, пожалуйста, отправьте им это письмо. Мы будем рады любым отзывам и замечаниям.
Эталонная реализация на Java
По ходу работы над новым вариантом статьи мы разбирались с алгоритмом, чтобы написать эталонную реализацию на Java. У нас получилось! Первую версию приложения мы опубликовали 19 ноября на github под лицензией LGPL version 3:
Reference Implementation of Romanov's Polynomial Algorithm for Boolean 3-SAT Problem
github.com/anjlab/sat3
Сейчас это однопоточная реализация, представляющая собой консольное приложение, которое читает формулы из файлов формата DIMACS CNF и выдает на выходе выполняющий набор если формула выполнима, или выдает соответствующее сообщение, если формула не выполнима. Программа ведет подробный лог, который должен помочь читателям статьи разобраться в работе алгоритма.
Для затравки, вот базисный граф с выполняющим набором для примера из статьи (слева) и для формулы с количеством переменных равным 100 (справа, кликабельно):
 |
 |
Подробнее описание результатов работы приложения можно найти здесь. Там же на github есть readme и несколько страничек в wiki с пояснениями как запустить приложение.
Последняя опубликованная версия — 1.0.3. Но в HEAD лежат несколько дополнительных оптимизаций, которые ускоряют работу приложения в 2 раза (версия 2.0.0-SNAPSHOT).
Что дальше
Дальнейшая работа может быть разделена на несколько направлений.
- Популяризация статьи, с целью показать ее как можно большему числу заинтересованных людей.
Здесь я надеюсь на помощь Хабра. Также мы будем работать над публикацией статьи в научный журнал, у нас сейчас есть несколько вариантов.
- Создание производительной реализации.
Эталонная реализация изначально задумывалась как помощь читателям в ознакомлении с работой алгоритма. Предполагалось, чтобы она могла работать на любом персональном компьютере, где можно запустить Java. Она не рассчитана на решение промышленных задач большой размерности.
С одной стороны этому мешает вычислительная сложность алгоритма (O(n^4*m)), с другой стороны — ресурсные ограничения, в частности, оперативная память. Здесь есть несколько путей развития: оптимизация структур данных и алгоритмов, и распараллеливание алгоритма (на несколько потоков, процессов и т.д.).
Если у вас есть желание помочь с этим — пишите, будем искать способы сотрудничества.
- Решение прикладных задач.
Сама по себе задача 3-ВЫП чисто теоретическая, но к ней сводятся многие другие прикладные задачи. Хотя это уже тема отдельных исследований.
