Тополь, «Любожид». Хотя конечно это пересказ городских легенд, в обсуждениях считают что это никогда не работало, а после 90го (когда борьба с отмыванием и т.п.), это совершенно невозможно. Ну и отдельно есть наказание за «…whoever mutilates, cuts, disfigures, perforates, unites or cements together, or does any other thing to any bank bill, draft, note, or other evidence of debt issued by… imprisoned not more than six months…»
Ну и в целом там наверно больше Isabelle, что-то там совместно с микрософтом по Z3.
Могу поспрашивать, наверно, если что, как я уже сказал, я в этом не специалист, только сам пытаюсь разобраться…
Презентованное там почти всегда применяется в каких-то проектах и продуктах, институт ведет множество таковых, «чистой науки для души» там практически нет. Есть и проекты для верификации ОСРВ и сертифицированной авионики в частности… но тут я только знаю, что они есть (тут я не очень в теме, а для меня верификация это пока хобби и в основном в части автоматических доказательств).
К чему это я — может стоит убрать риторический абзац о «пыльных трудах института системного программирования РАН»? По моему мнению, условных 95% открывших эту статью, прочтут пару первых вводных абзацев с игривым тоном, и не полезут в скучные подробности, не говоря уже о комментариях. Но где-то этот абзац отложится, с меткой «на хабре считают что…». Это же нехорошо.
«Затем наступают «темные века», которых найти не удается, и потом в 2017 году снова появляются материалы»
— возможно вы зашли на страницу «последних выпусков» (там номера с 2017), но не прошли по ссылке «полный архив» ← там номера с 2000 → и вот так, появилась «хронология Скалигера с темными веками». На всякий случай, для прохожих — это не так, проекты и темы (особенно по верификации), в ИСПРАНе развивались методично и равномерно. Кроме статей, часто получалось, когда я снимал разные доклады, что именно по темам верификации, включая весьма прикладные аспекты, именно ИСПРАНовские ребята попадались чаще всего.
Видимо, под трудами ИСПРАН вы имели в виду любое творчество, как-то сводимое к сотрудникам ИСПРАН (ну да, есть пожилые сотрудники, у них были относительно олдскульные курсы для младшекурсников, возможно вы наткнулись на курсы Л×××ва, или Л×××вой) — именно это предпредложение я добавил в комментарий (не хотел дробить). Но Труды ИСПРАН это вполне определенный рецензируемый журнал, и если там проходит дичь и древности по верификации, мне это было бы интересно — я смог бы найти рецензентов, ну и повлиять, чтобы никогда. А так, по моим данным, уровень проектов, тем, технологий по верификации там вполне на уровне.
Уверяю, не хотел никого обидеть. Хотя ваше утверждение «пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» как раз является панибратским и менторским, и, по-моему мнению, действительно может кого-то обидеть.
«пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» — это для красного словца, или можете привести хотя бы отдельные примеры (не говоря уж о «при этих словах люди начинают думать»)? Да-да, по теме «верификация ПО». Я наверно знаю про пару пожилых сотрудников (Е.Л.), которые наверное могут что-то совсем олдскульное написать, но вдруг реально проблема и с молодежью, и действительно все плохо, серьезно, просветите.
http://0x1.tv/Poisson-burning-time-agiledays-lighting-talk Не устаревший блиц-доклад, обосновывающий «умножение на Pi», тремя разными моделями реализации проекта (пуассоновский поток, логнормальное распределение, броуновское движение)
Нет, я как раз писал коммент для тех, кто совсем не в курсе теории сложности, для кого даже NP-задачи «плохие, потому что НеПэ». Пусть программист-практик не занимается сводимостями, а просто ищет свою задачу в компендиуме, главное помнить, что тут не ситуация с «двумя стульями» (либо решаем маленькую и точно, либо большую, но без гарантий), и для NP-сложных задач можно ожидать эффективных апроксимаций или вероятностных алгоритмов, возможно для этого просто нужно обнаружить в задаче дополнительные условия (ну или чуть-чуть выкрутить ей руки). Например понять, что TSP на реальных картах скорее всего всегда метрическая, и т.п.
В процессе использования я наткнулся на проблему: некоторые сайты имеют интересные требования к паролям
А это на самом деле — главное. Даже один из самых первых JS-хеширующих-букмарклетов (лет 12 ему, если не больше) https://github.com/chriszarate/supergenpass, сразу заморачивался этой проблемой (насколько помню, продолжал хешировать пока не выпадет большая+малая+цифра).
Как-то очень странно, столкнувшись с NP-полной задачей, сразу сдаваться и переходить, как рекомендуется в чеклисте, к эвристикам (т.е. алгоритмам без хоть каких-то гарантированных оценок качества оптимизации).
Ведь можно еще
Проверить, не попадает ли задача в APX-полные? (если да, то плохо с приближенными алгоритмами, да, но тоже не повод бежать в эвристики сразу).
Если нет — поискать FPTAS или хотя бы PTAS алгоритмы (NP-полный рюкзак можно оптимизировать сколь угодно точно для любого епсилон за n^2/eps, может уже и дешевле).
Если нет FPTAS, и PTAS — можно поискать оптимизацию к константной точностью, как в алгоритме Кристофидеса для метрической TSP (ну или даже логарифмической — жадный для упаковки например). Имея гарантии, что решение будет не хуже чем в 3/2 или 1/2 раз хуже, а для почти всех нормальных распределений — что-то близкое к оптимальному — очень даже неплохо и очень часто сгодится на практике вместо точного.
Можно покопать вероятностные алгоритмы — у них могут быть хорошие оценки в среднем (по качеству, по времени), или оценки «для почти всех исходных данных».
Можно посмотреть на входные данные внимательно, и понять, что экспоненциальные в худшем случае алгоритмы тут будут хороши и доказуемо полиномиальны в среднем (какое-нибудь динамическое программирование, где набор частичных решений окажется в среднем полиномом или константой) …
…
…
И уж если ничего вообще честного не получится, тогда да, умывайте руки и тащите эвристики.
По моему опыту, хуже всего с «Win10 64bit гостями» — неделями перебирал опции, даже с самой жалкой и беззубой конфигурацией — рандомные бсоды и зависания.
Доклад несколько двухлетней давности, если тема Альта на Эльбрусе интересна, то по ссылке полно и более свежих докладов (ну там, чтобы не гнать глупости про патченный gcc например).
Конечно, несколько грустно сознавать, что есть чуть ли не на порядок разрыв в ценах между малосерийными эльбрусами и майнстримом X86, что приходится переизобретать майнфреймы, чтобы этот геп закрыть. В кулуарах конференций обсуждается продвижение инициативы прямого спонсирования покупки эльбрусов (ну, фиксируется цена X и в течении скажем трех лет, цена выше X потребителю компенсируется).
У меня в квартире 140м все было в светодиодных светильниках Feron и Sonex.
За год
у одного сонекса сдохло ДУ
два сонекса перегорели (к сожалению не светодиод, а именно блоки).
штук у 4 Feronов (небольшие-точечные) сдохли БД (мерцание адово).
** пластик у них тоже отстой, у нескольких точечных отваливались (отклеивались) рассеиватели.
Если кто знает, где гарантийный ремонт Сонексов, плиз, напишите.
Эх, а сколько было пафосных докладов на конференциях (http://youtu.be/_WFcarwN4Ao, https://vimeo.com/129710774, … ) где на удивление зрителей («вы это сделали чтобы что?») презрительно щурились «вам не понять хитроплан».
Ага, спасибо. Может тогда вы сможете потестировать несколько Goovis-ов (у них несколько продуктов, сходу непонятно в чем фишка каждого), и именно с этой стороны (чтение). Я тогда начну мечтать и отслеживать самый подходящий б.у. девайс на ебее..
Все-таки заходя в статью с названием «Разбор решения задач…» ожидаешь увидеть код, ссылки на код… а не «фоточки с ивента».
Грустно, что вы не публикуете код решений, при том, что считаете права на него своими.
Ну возможно кого-то заинтересует именно видео доклада Зураба по этой теме → http://www.0x1.tv/20191114AM (слабовидящие, желающие подкрепится харизмой докладчика и т.п.)
Тополь, «Любожид». Хотя конечно это пересказ городских легенд, в обсуждениях считают что это никогда не работало, а после 90го (когда борьба с отмыванием и т.п.), это совершенно невозможно. Ну и отдельно есть наказание за «…whoever mutilates, cuts, disfigures, perforates, unites or cements together, or does any other thing to any bank bill, draft, note, or other evidence of debt issued by… imprisoned not more than six months…»
Что-то в тиньков банке даже, судя по курсам, в хуавее русском… не только жетбрейнс.
Курс по алгоритмам, 6 курс, ФУПМ. Или я ошибся?
Привет (если меня помните)!
Ну вместо названий наверно интересней конкретные фамилии, давайте зацепимся в поиске за http://www.mathnet.ru/php/person.phtml?option_lang=rus&personid=125232 например.
(наверно это группа Петренко… но не уверен).
Ну и в целом там наверно больше Isabelle, что-то там совместно с микрософтом по Z3.
Могу поспрашивать, наверно, если что, как я уже сказал, я в этом не специалист, только сам пытаюсь разобраться…
Презентованное там почти всегда применяется в каких-то проектах и продуктах, институт ведет множество таковых, «чистой науки для души» там практически нет. Есть и проекты для верификации ОСРВ и сертифицированной авионики в частности… но тут я только знаю, что они есть (тут я не очень в теме, а для меня верификация это пока хобби и в основном в части автоматических доказательств).
К чему это я — может стоит убрать риторический абзац о «пыльных трудах института системного программирования РАН»? По моему мнению, условных 95% открывших эту статью, прочтут пару первых вводных абзацев с игривым тоном, и не полезут в скучные подробности, не говоря уже о комментариях. Но где-то этот абзац отложится, с меткой «на хабре считают что…». Это же нехорошо.
— возможно вы зашли на страницу «последних выпусков» (там номера с 2017), но не прошли по ссылке «полный архив» ← там номера с 2000 → и вот так, появилась «хронология Скалигера с темными веками». На всякий случай, для прохожих — это не так, проекты и темы (особенно по верификации), в ИСПРАНе развивались методично и равномерно. Кроме статей, часто получалось, когда я снимал разные доклады, что именно по темам верификации, включая весьма прикладные аспекты, именно ИСПРАНовские ребята попадались чаще всего.
Видимо, под трудами ИСПРАН вы имели в виду любое творчество, как-то сводимое к сотрудникам ИСПРАН (ну да, есть пожилые сотрудники, у них были относительно олдскульные курсы для младшекурсников, возможно вы наткнулись на курсы Л×××ва, или Л×××вой) — именно это предпредложение я добавил в комментарий (не хотел дробить). Но Труды ИСПРАН это вполне определенный рецензируемый журнал, и если там проходит дичь и древности по верификации, мне это было бы интересно — я смог бы найти рецензентов, ну и повлиять, чтобы никогда. А так, по моим данным, уровень проектов, тем, технологий по верификации там вполне на уровне.
Уверяю, не хотел никого обидеть. Хотя ваше утверждение «пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» как раз является панибратским и менторским, и, по-моему мнению, действительно может кого-то обидеть.
«пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» — это для красного словца, или можете привести хотя бы отдельные примеры (не говоря уж о «при этих словах люди начинают думать»)? Да-да, по теме «верификация ПО». Я наверно знаю про пару пожилых сотрудников (Е.Л.), которые наверное могут что-то совсем олдскульное написать, но вдруг реально проблема и с молодежью, и действительно все плохо, серьезно, просветите.
http://0x1.tv/Poisson-burning-time-agiledays-lighting-talk Не устаревший блиц-доклад, обосновывающий «умножение на Pi», тремя разными моделями реализации проекта (пуассоновский поток, логнормальное распределение, броуновское движение)
Нет, я как раз писал коммент для тех, кто совсем не в курсе теории сложности, для кого даже NP-задачи «плохие, потому что НеПэ». Пусть программист-практик не занимается сводимостями, а просто ищет свою задачу в компендиуме, главное помнить, что тут не ситуация с «двумя стульями» (либо решаем маленькую и точно, либо большую, но без гарантий), и для NP-сложных задач можно ожидать эффективных апроксимаций или вероятностных алгоритмов, возможно для этого просто нужно обнаружить в задаче дополнительные условия (ну или чуть-чуть выкрутить ей руки). Например понять, что TSP на реальных картах скорее всего всегда метрическая, и т.п.
А это на самом деле — главное. Даже один из самых первых JS-хеширующих-букмарклетов (лет 12 ему, если не больше)
https://github.com/chriszarate/supergenpass, сразу заморачивался этой проблемой (насколько помню, продолжал хешировать пока не выпадет большая+малая+цифра).
Как-то очень странно, столкнувшись с NP-полной задачей, сразу сдаваться и переходить, как рекомендуется в чеклисте, к эвристикам (т.е. алгоритмам без хоть каких-то гарантированных оценок качества оптимизации).
Ведь можно еще
…
…
И уж если ничего вообще честного не получится, тогда да, умывайте руки и тащите эвристики.
Он делает это чрезвычайно плохо (экспериментальная неработающая фича).
По моему опыту, хуже всего с «Win10 64bit гостями» — неделями перебирал опции, даже с самой жалкой и беззубой конфигурацией — рандомные бсоды и зависания.
У меня в квартире 140м все было в светодиодных светильниках Feron и Sonex.
За год
** пластик у них тоже отстой, у нескольких точечных отваливались (отклеивались) рассеиватели.
Если кто знает, где гарантийный ремонт Сонексов, плиз, напишите.
Эх, а сколько было пафосных докладов на конференциях (http://youtu.be/_WFcarwN4Ao, https://vimeo.com/129710774, … ) где на удивление зрителей («вы это сделали чтобы что?») презрительно щурились «вам не понять хитроплан».
Ага, спасибо. Может тогда вы сможете потестировать несколько Goovis-ов (у них несколько продуктов, сходу непонятно в чем фишка каждого), и именно с этой стороны (чтение). Я тогда начну мечтать и отслеживать самый подходящий б.у. девайс на ебее..
Все-таки заходя в статью с названием «Разбор решения задач…» ожидаешь увидеть код, ссылки на код… а не «фоточки с ивента».
Грустно, что вы не публикуете код решений, при том, что считаете права на него своими.
Ну возможно кого-то заинтересует именно видео доклада Зураба по этой теме → http://www.0x1.tv/20191114AM (слабовидящие, желающие подкрепится харизмой докладчика и т.п.)