Логи это конечно хорошо, если там есть предупреждение или можно по логам сориентироваться в контексте. Но все значения переменных, условия и циклы в логах не вывести.
Такие ставки не только в вашем вузе. По-крайней мере, во Владимирском госуниверситете такие же.
Насколько я знаю это ставка только за аудиторные часы.
Например,
> профессора — 7260, зав.кафа — 7735
Если зав. кафедрой еще и профессор, то у него ставка будет 7260+7735=14995. Первое — за лекции, второе за руководство кафедрой.
С надбавками (работа с контрактниками, руководство дипломниками, кандидатами, курсовыми работами и пр.) получается 10-20 тыс; 20-30 тыс. — встречается крайне редко.
Но помимо таких надбавок есть еще всякие НИР и прочая деятельность, которая приносит дополнительный доход, никак не связанный с учебным процессом. Автор топика, вот, например, на вторые полставки работает в другом месте. Тоже самое практически со всем профессорско-преподавательским составом.
Fatal error: Uncaught exception 'Exception' with message 'DateTimeZone::__construct() [<a href='datetimezone.--construct'>datetimezone.--construct</a>]: Unknown or bad timezone ()' in /usr/local/data/www/data-segodnya.ru/index.php:54 Stack trace: #0 /usr/local/data/www/data-segodnya.ru/index.php(54): DateTimeZone->__construct('') #1 {main} thrown in /usr/local/data/www/data-segodnya.ru/index.php on line 54
Павел, я бы подписался под каждым пунктом, где речь идет о разработке.
Но если говорить о первом запросе:
Нам нужны специалисты в различных областях (в первую очередь, в области информационых технологий), которые могли бы грамотно и доходчиво написать экспертное заключение, поясняющее, почему тот или иной конкурс является распилом. Необходимо на конкретных примерах из ТЗ показать почему за положенное время невозможно выполнить необходимую работу.
… работа с конкурсной документацией (КД) и написание экспертного заключения — это немного другая работа. По сути, чтобы сказать почему конкурс является роспилом, надо написать собственное предложение-заявку на каждый такой конкурс и посмотреть насколько отличаются рассчеты. А для этого уже нужно проанализировать КД (это может быть большой документ на десятки страниц), возможно, сделать запросы на разъяснение положений организатору конкурса, перебрать массу вариантов решений и выбрать один. Это не очень приятная работа, которую можно списать на open source just for fun.
Если отвлечься от вопроса «бесплатных экспертов», то вроде бы и не нужно быть большим экспертом, чтобы заметить, что ИТ-конкурс является роспилом: там обычно просто несоизмеримо маленькие сроки при большом объеме работ.
Я думаю можно даже какой-то коэффициент вывести среднеотраслевой (например, по моему мнению индикатором роспила будет проект, который стоит в среднем больше 500-800 тыс. рублей в месяц и при этом занимает по срокам меньше двух месяцев), хотя обычно достаточно здравого смысла, чтобы понять, что:
Нельзя сделать большой ИТ-проект в сжатые сроки, если только речь не идет просто о закупке готового дорогостоящего ПО или оборудования по прайсу.
Я переговорил с Владимиром Федоровичем. По первому вопросу все так: если две переменные будут иметь разные значения — это приведет к противоречию и совместного выполняющего набора для них быть не может по построению. По второму — тройки переменных отдельно не нужно проверять, потому что такая проверка покрываются проверкой пар значений переменных. Если в двух тройках любая пара совпадает, значит и тройки тоже совпадают.
Насчет скорости: помимо n и m на время работы алгоритма влияет еще структура формулы. Некоторые формулы можно декомпозировать на 2 ФКТ, другие — на 10, третьи — на сотни. Время работы алгоритма будет также зависеть от числа k — количества ФКТ. Это число неявно присутствует в оценке сложности в качестве m: O(m * n^4). Соответственно, чем больше k, чем больше в базисной СКТ строк — тем дольше будет работать алгоритм.
Еще один момент: в приложении реализованы два алгоритма, которые запускаются последовательно. Первый — построение системы гиперструктур. Если результатом его работы является напустая HSS, то формула считается выполнимой по теореме 1.
Второй алгоритм — поиск выполняющего набора в HSS. Вообще говоря в статье этот алгоритм не рассматривается. Сейчас в реализации он работает так: в HSS последовательно из каждого уровня базисного графа отбрасываются все вершины кроме одной начиная с первого уровня и так далее вниз. Оставляется только одна вершина (любая), подструктура которой имеет непустое пересечение с любой подструктурой вершины последнего уровня. Строится новая система гиперструктур. Дальше со второго уровня выбрасываются все вершины, кроме смежных с вершиной первого уровня. Их максимум две. Какую оставить решает такое правило: оставляем первую вершину и строим систему HSS, если она построена — значит мы выбрали правильную вершину, если нет — значит оставляем вторую вершину. И так далее, пока HSS не станет элементарной, то есть будет содержать только одно j-пересечение.
К чему я это, к тому, что при запуске алгоритма HSS может строиться несколько раз — что приводит к еще более длительному времени работы программы. Почему может — потому что сейчас не обязательно HSS сводить к элементарной для поиска выполняющего набора, так как там есть вспомогательный алгоритм (quickFindHSSRoute), который умеет находить выполняющий набор в системе гиперструктур. Не буду вдаваться в подробности этого алгоритма, можно считать сейчас, что это эвристика.
Насчет второго вопроса, я уточню у Владимира Федоровича. Но вроде бы так:
второе доказательство строится на одноименных j-пересечениях; унификация, как она определена, должна приводить к тому, чтобы в двух CTS убирались строки, которые не образуют совместного выполняющего набора.
В алгоритме SEP пункт A concordance rules на стр. 15 говорит о том, что все одноименные подструктуры должны быть унифицированы в ходе построения HSS. Это приводит к тому, что все одноименные j-пересечения будут в себе заключать все совместные выполняющие наборы.
тройки битов не проверяются, потому что подразумевается, что три переменных в одной тройке могут быть только в одной СКТ.
Конечно, там есть и большие формулы — они использовались в основном в начале разработки для тестирования алгоритма декомпозиции формулы. Но есть экземпляры и поменьше, например, article-example.cnf — это формула из статьи, cnf-v112-c418-100-sat.cnf — формула, которая нашим алгоритмом декомпозируется на 2 ФКТ, так что получается одна гиперструктура, и т.д. Большинство формул для тестов были взяты отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
Я не запускал регрессионные тесты на всех формулах, потому что есть набор unit-тестов, которые тестируют разные алгоритмы по-отдельности.
Насчет решения — их обычно быть много, можно конечно привести одно, но зачем? Если вы получите свое — можете легко его проверить, подставив значения в формулу.
Очень может быть. Вообще, Романов сам постоянно говорит, что наверняка все можно сделать проще, найти какие-то свойства структур и алгоритмов, которые позволят сделать его эффективнее. Но для доказательства уже достаточно того, что есть сейчас. В статье про унификацию вообще приводятся только основные правила, суть которых показать какой должен быть результат. Как это будет реализовано — другой вопрос. Только я переписывал процедуру унификации несколько раз. Правда со стороны, которую предлагаете вы, я на эту проблему не смотрел. Интересно.
1. Подобного представления формул (в виде компактных троек) еще ни у кого не было — это оригинальный подход.
2. Сама идея и алгоритм были придуманы и описаны 10 лет назад. Просто почему-то ее никто до этого не замечал. Владимир Федорович занимался решением этой задачи независимо от своей основной работы, ни в рамках какого-то научного проекта, а просто так — как хобби (кстати начал он ее еще в 90-х). У нас на кафедре про его работу знали, но за рамки кафедры эти знания так и не вышли, если не считать единичных публикаций в вузовских сборниках и переписок один-на-один с рецензентами, которые привели к статье в непрофильном журнале.
Тот факт, что про эту статью узнали сейчас — это чистая случайность. Если бы не нашумевшая история о Деолаликаре, то прошло бы еще 10 лет и так ничего бы не изменилось. Именно эта история сыграла для меня решающую роль. Как так! Его статью обсудили и знают, а о статье Романова за 10 лет так никто и не узнал. Только из-за этого я решил потратить несколько месяцев работы, чтобы вместе с Романовым еще раз перечитать его статью, отредактировать английский вариант, сделать версию в LaTeX (это вообще отдельная история), разобраться в алгоритме, написать реализацию, написать письмо, найти адреса ученых и отправить это письмо им. Но это все было как хобби. Работа никем не спонсировалось, все делалось в свободное время. (Вообще-то я думал на это уйдет меньше времени.) А что получается в итоге? В итоге все уже сыты по-горло подобными доказательствами и я прекрасно понимаю, почему ни у кого нет желания разбираться в этой работе и понимаю скепсицизм с которым к работе относятся.
Судить не мне, но я считаю, что лучше, чтобы о статье узнали поздно чем никогда. А уж верна она или нет — покажет время. Хорошо, что ее уже включили в знаменитый список The P-versus-NP page. Правда под номером 65 и с датой 20 ноября, хотя должны бы были включить в первую пятерку или десятку и с годом 2002.
Не уверен, что понял вопрос про унификацию.
Унификация не имеет дело с тройками — только с парами переменных и с переменными, которые тождественно 1 или 0.
Если переменные x1 и x2 встречаются в пределах одной тройки в двух и более структурах — значит при унификации нужно учитывать эту пару.
Не понял про фиктивные переменные, зачем их добавлять? В любом случае, если вы добавляете «фиктивные» переменные, то они также участвуют в процедурах очищения и унификации.
Программа собирается maven3 (но я думаю можно и maven2), я запускаю тест из eclipse.
Чтобы загрузить проект в эклипс делаете checkout, потом в этой папке запускаете (maven2/3 должен быть в переменной PATH):
mvn clean test
Все тесты должны пройти. После этого можно загрузить проект в IDE, чтобы загрузить в eclipse я делаю так:
1)
mvn eclipse:eclipse
2) В eclipse делаю File -> Import -> Existing projects into workspace… -> Выбираю оба проекта 3-sat-core и 3-sat-experiment
3) Дальше нужно будет добавить переменную билда M2_REPO. Для этого на проекте нужно щелкнуть правой кнопкой -> Properties -> Java Build Path -> На вкладке Libraries нажать кнопку Add Variable… -> Configure Variables… -> New… -> В качестве имени M2_REPO, значение — путь к папке с репозиторем maven2, по умолчанию он в <user-dir>/m2/repository (например, c:\Users\dmitrygusev\.m2\repository) -> Дальше везде Ok
Да, базисная структура там другая получилась.
Алгоритм выбирает базисную структуру по простому правилу — где меньше строк.
Если это принципиально (это сказывается только на потреблении памяти).
Я могу переписать тест, чтобы можно было явно базисную структуру задавать.
Как решим?
Пишите сколько получается, а не супер надбавку, которая даже не превышает прожиточного минимума.
Насколько я знаю это ставка только за аудиторные часы.
Например,
> профессора — 7260, зав.кафа — 7735
Если зав. кафедрой еще и профессор, то у него ставка будет 7260+7735=14995. Первое — за лекции, второе за руководство кафедрой.
С надбавками (работа с контрактниками, руководство дипломниками, кандидатами, курсовыми работами и пр.) получается 10-20 тыс; 20-30 тыс. — встречается крайне редко.
Но помимо таких надбавок есть еще всякие НИР и прочая деятельность, которая приносит дополнительный доход, никак не связанный с учебным процессом. Автор топика, вот, например, на вторые полставки работает в другом месте. Тоже самое практически со всем профессорско-преподавательским составом.
Fatal error: Uncaught exception 'Exception' with message 'DateTimeZone::__construct() [<a href='datetimezone.--construct'>datetimezone.--construct</a>]: Unknown or bad timezone ()' in /usr/local/data/www/data-segodnya.ru/index.php:54 Stack trace: #0 /usr/local/data/www/data-segodnya.ru/index.php(54): DateTimeZone->__construct('') #1 {main} thrown in /usr/local/data/www/data-segodnya.ru/index.php on line 54Например, чтобы можно было разместить у себя кнопку «я пойду».
Но если говорить о первом запросе:
… работа с конкурсной документацией (КД) и написание экспертного заключения — это немного другая работа. По сути, чтобы сказать почему конкурс является роспилом, надо написать собственное предложение-заявку на каждый такой конкурс и посмотреть насколько отличаются рассчеты. А для этого уже нужно проанализировать КД (это может быть большой документ на десятки страниц), возможно, сделать запросы на разъяснение положений организатору конкурса, перебрать массу вариантов решений и выбрать один. Это не очень приятная работа, которую можно списать на open source just for fun.
Если отвлечься от вопроса «бесплатных экспертов», то вроде бы и не нужно быть большим экспертом, чтобы заметить, что ИТ-конкурс является роспилом: там обычно просто несоизмеримо маленькие сроки при большом объеме работ.
Я думаю можно даже какой-то коэффициент вывести среднеотраслевой (например, по моему мнению индикатором роспила будет проект, который стоит в среднем больше 500-800 тыс. рублей в месяц и при этом занимает по срокам меньше двух месяцев), хотя обычно достаточно здравого смысла, чтобы понять, что:
Нельзя сделать большой ИТ-проект в сжатые сроки, если только речь не идет просто о закупке готового дорогостоящего ПО или оборудования по прайсу.
Еще один момент: в приложении реализованы два алгоритма, которые запускаются последовательно. Первый — построение системы гиперструктур. Если результатом его работы является напустая HSS, то формула считается выполнимой по теореме 1.
Второй алгоритм — поиск выполняющего набора в HSS. Вообще говоря в статье этот алгоритм не рассматривается. Сейчас в реализации он работает так: в HSS последовательно из каждого уровня базисного графа отбрасываются все вершины кроме одной начиная с первого уровня и так далее вниз. Оставляется только одна вершина (любая), подструктура которой имеет непустое пересечение с любой подструктурой вершины последнего уровня. Строится новая система гиперструктур. Дальше со второго уровня выбрасываются все вершины, кроме смежных с вершиной первого уровня. Их максимум две. Какую оставить решает такое правило: оставляем первую вершину и строим систему HSS, если она построена — значит мы выбрали правильную вершину, если нет — значит оставляем вторую вершину. И так далее, пока HSS не станет элементарной, то есть будет содержать только одно j-пересечение.
К чему я это, к тому, что при запуске алгоритма HSS может строиться несколько раз — что приводит к еще более длительному времени работы программы. Почему может — потому что сейчас не обязательно HSS сводить к элементарной для поиска выполняющего набора, так как там есть вспомогательный алгоритм (quickFindHSSRoute), который умеет находить выполняющий набор в системе гиперструктур. Не буду вдаваться в подробности этого алгоритма, можно считать сейчас, что это эвристика.
Насчет второго вопроса, я уточню у Владимира Федоровича. Но вроде бы так:
В алгоритме SEP пункт A concordance rules на стр. 15 говорит о том, что все одноименные подструктуры должны быть унифицированы в ходе построения HSS. Это приводит к тому, что все одноименные j-пересечения будут в себе заключать все совместные выполняющие наборы.
Конечно, там есть и большие формулы — они использовались в основном в начале разработки для тестирования алгоритма декомпозиции формулы. Но есть экземпляры и поменьше, например, article-example.cnf — это формула из статьи, cnf-v112-c418-100-sat.cnf — формула, которая нашим алгоритмом декомпозируется на 2 ФКТ, так что получается одна гиперструктура, и т.д. Большинство формул для тестов были взяты отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
Я не запускал регрессионные тесты на всех формулах, потому что есть набор unit-тестов, которые тестируют разные алгоритмы по-отдельности.
Насчет решения — их обычно быть много, можно конечно привести одно, но зачем? Если вы получите свое — можете легко его проверить, подставив значения в формулу.
1. Подобного представления формул (в виде компактных троек) еще ни у кого не было — это оригинальный подход.
2. Сама идея и алгоритм были придуманы и описаны 10 лет назад. Просто почему-то ее никто до этого не замечал. Владимир Федорович занимался решением этой задачи независимо от своей основной работы, ни в рамках какого-то научного проекта, а просто так — как хобби (кстати начал он ее еще в 90-х). У нас на кафедре про его работу знали, но за рамки кафедры эти знания так и не вышли, если не считать единичных публикаций в вузовских сборниках и переписок один-на-один с рецензентами, которые привели к статье в непрофильном журнале.
Тот факт, что про эту статью узнали сейчас — это чистая случайность. Если бы не нашумевшая история о Деолаликаре, то прошло бы еще 10 лет и так ничего бы не изменилось. Именно эта история сыграла для меня решающую роль. Как так! Его статью обсудили и знают, а о статье Романова за 10 лет так никто и не узнал. Только из-за этого я решил потратить несколько месяцев работы, чтобы вместе с Романовым еще раз перечитать его статью, отредактировать английский вариант, сделать версию в LaTeX (это вообще отдельная история), разобраться в алгоритме, написать реализацию, написать письмо, найти адреса ученых и отправить это письмо им. Но это все было как хобби. Работа никем не спонсировалось, все делалось в свободное время. (Вообще-то я думал на это уйдет меньше времени.) А что получается в итоге? В итоге все уже сыты по-горло подобными доказательствами и я прекрасно понимаю, почему ни у кого нет желания разбираться в этой работе и понимаю скепсицизм с которым к работе относятся.
Судить не мне, но я считаю, что лучше, чтобы о статье узнали поздно чем никогда. А уж верна она или нет — покажет время. Хорошо, что ее уже включили в знаменитый список The P-versus-NP page. Правда под номером 65 и с датой 20 ноября, хотя должны бы были включить в первую пятерку или десятку и с годом 2002.
Нет, наверное все так. Я просто не понимаю к чему это… :\
Унификация не имеет дело с тройками — только с парами переменных и с переменными, которые тождественно 1 или 0.
Если переменные x1 и x2 встречаются в пределах одной тройки в двух и более структурах — значит при унификации нужно учитывать эту пару.
Не понял про фиктивные переменные, зачем их добавлять? В любом случае, если вы добавляете «фиктивные» переменные, то они также участвуют в процедурах очищения и унификации.
Тест был у меня в рабочей копии, сейчас я его закомитил: github.com/anjlab/sat3/commit/27e75ae4527f15ae0d6e3dedb98dccc948f1cc74
Программа собирается maven3 (но я думаю можно и maven2), я запускаю тест из eclipse.
Чтобы загрузить проект в эклипс делаете checkout, потом в этой папке запускаете (maven2/3 должен быть в переменной PATH):
Все тесты должны пройти. После этого можно загрузить проект в IDE, чтобы загрузить в eclipse я делаю так:
1)
2) В eclipse делаю File -> Import -> Existing projects into workspace… -> Выбираю оба проекта 3-sat-core и 3-sat-experiment
3) Дальше нужно будет добавить переменную билда M2_REPO. Для этого на проекте нужно щелкнуть правой кнопкой -> Properties -> Java Build Path -> На вкладке Libraries нажать кнопку Add Variable… -> Configure Variables… -> New… -> В качестве имени M2_REPO, значение — путь к папке с репозиторем maven2, по умолчанию он в <user-dir>/m2/repository (например, c:\Users\dmitrygusev\.m2\repository) -> Дальше везде Ok
Алгоритм выбирает базисную структуру по простому правилу — где меньше строк.
Если это принципиально (это сказывается только на потреблении памяти).
Я могу переписать тест, чтобы можно было явно базисную структуру задавать.
Как решим?