2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Доказательство доказательства
Сообщение12.09.2016, 07:37 


12/09/16
3
Есть некая сложная задача. Допустим она решаема за разумное, хотя и большое время, на ПК при помощи SAT решателя. По окончанию решения будет получен контрпример или ответ НЕТ. В случае получения ответа НЕТ, как мне доказать людям, что я решил задачу (что я вообще ее решал, а не просто заявил, что контрпример не найден)?


PS: Вопрос не про корректность доказательства на ПК. Просто я в раздумьях браться за это дело или нет. На написание программы ( там не только решатель ) уйдет много сил, а потом еще длительная работа решателя. А по окончанию люди начнут мне говорить, что ты мол, ничего не доказывал, а так просто заявил.

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 07:59 
Аватара пользователя


21/09/12

1871
Если к вашему результату отнесутся серьёзно, постараются разобраться в вашей программе. Проверят контрольными прогонами.
Если же программа и её идеи столь сложны, что желающих - и могущих - разобраться в них не находится, то это становится проблемой автора. Всё-таки придётся построить удобоваримую конструкцию, понятную близким специалистам.

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 08:47 
Заслуженный участник
Аватара пользователя


06/10/08
6422
ser.shvezov в сообщении #1150676 писал(а):
По окончанию решения будет получен контрпример или ответ НЕТ. В случае получения ответа НЕТ, как мне доказать людям, что я решил задачу (что я вообще ее решал, а не просто заявил, что контрпример не найден)?
Многие SAT-решатели умеют выдавать какие-то сертификаты неразрешимости.

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 09:06 


12/09/16
3
У меня свой SAT и он не выдает сертификатов.
И все таки может кто-то знает поподробнее про сертификаты неразрешимости?
Что-то я не нашел ..

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 09:47 
Заслуженный участник
Аватара пользователя


06/10/08
6422
ser.shvezov в сообщении #1150684 писал(а):
И все таки может кто-то знает поподробнее про сертификаты неразрешимости?
Вот описание формата, который используется в SAT Competition: https://www.cs.utexas.edu/~marijn/publi ... t-trim.pdf

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 12:55 


12/09/16
3
Xaositect
Спасибо!

Ох, если бы было все так просто.. Мой решатель не совсем SAT, он должен отбрасывать некоторые ветки по причинам учитывающим специфику задачи. Решать же чистую SAT задачу, невозможно по причине ее сложности.

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение12.09.2016, 16:45 
Заслуженный участник
Аватара пользователя


16/07/14
9147
Цюрих
В пределе - лог работы вашего решателя, и доказательство корректности его работы:)

(если бы существовал простой способ доказательства невыполнимости любой невыполнимой формулы, то было бы $NP  = coNP$, что маловероятно)

 Профиль  
                  
 
 Re: Доказательство доказательства
Сообщение28.10.2016, 19:25 


31/12/15

24
ser.shvezov в сообщении #1150676 писал(а):
как мне доказать людям, что я решил задачу?


ser.shvezov в сообщении #1150676 писал(а):
Просто я в раздумьях браться за это дело или нет.


Вы какие-то не те вопросы задаёте. Результат нужно сначала себе самому доказать, то есть вы должны искренне верить в правильность доказательства, прежде чем пытаться доказать кому-то ещё. Если программа закончит работу и не сможет построить контрпример - вы сможете сами искренне поверить соей собственной программе?

Возможны два варианта. Первый - писать программу, как можно проще - в надежде, что контрпример существует и рано или поздно программа его надёт. В общем случае я бы не рекомендовал так делать, но из своего собственного опыта могу сказать, что один раз я так сделал. Дописал заведомо неверную программу, которая не должна была работать. А она взяла - и построила контрпример. Результат вошёл в диссертацию и подсказал дальнейшие пути для исследования.

Второй вариант - писать программу настолько качественно и тестировать её настолько тщательно, чтобы в случае, если контрпримера она не сможет построить контрпример, вы сами для себя могли бы быть уверены, что контрпримера действительно не существует. Добиться этого можно разными путями, и это зависит от задачи.

Можно, например, включить в программу возможность по требованию распечатать тот или иной фрагмент вычислений, другими словами - контролировать информацию, записываемую в лог. Самый сложный - но одновременно самый надёжный способ, на мой взгляд - это распечатать лог в таком формате, чтобы его могла проверить какая-то стронняя, независимая программа. Проще на примере: пусть требуется в процессе вычисления решить уравнение f(x)=0. Если программа распечатает x, то сторонняя программа может этот x проверить - подставить в f и посмотреть, получится 0 или нет. Или, там, перебирает программа отображения и требует их взаимной однозначности - пусть (по требованию) она эти отображения распечатает, тогда сторонняя программа пусть (некоторые из) них проверяет на взаимную однозначность...

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

В идеале программа должна распечатывать доказательство на каком-либо диалекте языка исчисления предикатов первого уровня или на одном из языков, используемых для верификации - Coq, Isabella, какие там ещё есть? GNU Aris (шутка).

Либо, как я уже говорил, попробовать сначала по-простому поискать контрпримеры в частных случаях - как поступить, конечно, только вы сможете решить, и только полагаясь на интуицию. Не факт, что писать одновременно две программы, которые ещё работают за достаточное время, будет проще, чем искать доказательство аналитически - опять же, решить это можете только вы, интуитивно.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 8 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group