Алгоритмы *

Привет, Хабр! В команде ВКонтакте существует система управления репликацией и консенсусом в кластере, которая называется BARSiC (Binary Asynchronous Replication with Simple Consensus). Прежде всего она контролирует состав кластера, определяя, кто реплика, а кто — мастер. А при выходе мастера из строя реплики выбирают нового с непротиворечивой линейной историей. 

Для решения этой задачи команда ВКонтакте совместно с университетом ИТМО работали над научно-исследовательским проектом «Разработка моделей для верификации распределенных алгоритмов в системе BARSiC». В этой статье подробно расскажем о том, как мы в рамках проекта верифицировали выбранный для BARSiC алгоритм, и попутно исправили найденную в нём ошибку. 

Делая свой очередной пет-проект подумал, что мне нужна конкурентная очередь с приоритетами. Оказалось она была не нужна, но желание ее реализовать никуда не ушло.

Проведя небольшой поиск, нашел несколько научных статей с конкурентной реализацией и выбрал одну в качестве образцовой.

Потратив время и нервы на ее понимание и реализацию, был отрицательно удивлен результату: ее производительность хуже чем глобальная блокировка на всю структуру данных.

Здесь описал свою реализацию и сделал сравнение с блокирующей реализацией.
Критика (даже не конструктивная) приветствуется.

Статья является продолжением предыдущей статьи в рамках цикла статей, посвященных обработке больших и очень больших графов. В статье реализованы распределенные версии четырех классических алгоритмов: "Связные компоненты", "Кратчайшее расстояние", "Топологическая сортировка" и PageRank на Apache Spark DataFrame API. Алгоритмы составлены в соответствии с идеями популярного фреймворка распределенной обработки графов Pregel.

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

Всем привет! Решила я вернуться на Хабр с новым мини-проектом. Сегодня попробуем детектить дорожные знаки используя YOLOv8 на Google colab. Что ж, приступим!

В прошлой части мы рассмотрели однокубитные гейты и построили какие то элементарные программы на однокубитных гейтах. Пришло время перейти к многокубитным преобразованиям.

Квантовые гейты в случае многокубитных операций

Можно также рассмотреть каждый гейт с точки зрения матрицы преобразования. Но такое описание слишком громоздко. Например состояние из двух кубит:

Однажды ко мне обратилась одна крупная фруктовая телефонная компания с просьбой подготовить для них курс по Apache Spark продвинутого уровня, и в нем обязательно должен быть раздел про обработку графов (Neo4j не предлагать). На тот момент я знал про классические алгоритмы обработки графов на базе DFS (поиск в глубину) и BFS (поиск в ширину). При этом неотъемлемым условием применения того или иного подхода является локальная поддержка стека (DFS) или очереди (BFS). Следовательно, классические алгоритмы можно применять для обработки графов, которые умещаются в память одной машины.

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

Поиск контактных точек коллизии

Одна из важных тем при разработке своего физического движка - нахождение контактных точек. Применение этим данным масса - от определения центра удара, до построения градиента приложенных сил.

Давайте же посмотрим как это сделать!

До появления Такси, машину часто вызывали «от борта»: находили или останавливали такси и договаривались о цене и маршруте. Кто и как повезёт пассажира — тот ещё вопрос. Теперь с появлением агрегаторов требования к перевозкам сильно выросли. 

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

После того как я реально «подсел» на чтение Хабра, захотелось «освежить» что‑то из своего богатого математического прошлого. Воскресить, так сказать, старые наработки, зайдя, естественно, через дверь с табличкой Python. Предлагаемая публикация посвящена простейшим методам численного дифференцирования дискретных функций (они же решетчатые функции, они же табличные функции, они же функции, заданные набором данных и т. п.). Очень странно, что в библиотеках Python с такой простой темой не все так просто и безоблачно, есть кое‑какие вопросы и проблемы. SciPy, как оказалось, вообще не об этом, а в NumPy «тема не раскрыта». На простейших примерах рассмотрим то, что предлагает NumPy, что там не так и как можно сделать лучше.

В предыдущей статье мы познакомились с одним из представителей семейства «алгоритмов жука». Они прекрасно подходят для реализации функций передвижения относительно простых автономных мобильных устройств, оборудованных спартанским набором сенсорных датчиков. Однако не всё, что человек хотел бы переложить на хрупкие плечи бездушных железяк, реализуемо такими одиночными простейшими устройствами. И фантастическая литература, и научные изыскания твёрдо уверяют нас в перспективности роевых моделей для реализации сколь-нибудь сложных функциональностей.

Массивное распараллеливание и разделение общих задач, обеспечиваемое совместной работой простых механизмов, намного эффективнее и экономичнее использования одного более сложного. По этому поводу со времён товарища Форда ни у кого вопросов не возникает. А если посмотреть соревнования F1, то там это кажется настолько органичным, что будто по-другому и нельзя.

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

В настоящее время известно большое число систем счисления. Подробный перечень (не знаю, насколько полный) приведен в англоязычной Википедии. В этом списке я не нашел ту систему, которая будет изложена здесь. Она относится к классу систем с переменным основанием (mixed radix). Предлагаю ее назвать Flexible number system with a Prime Radixes, сокращенно FPR-системой счисления.

Но для того, чтобы ее понять, необходимы знания некоторых понятий алгебры кортежей (АК) и частично упорядоченных множеств хотя бы в том объеме, который имеется в соответствующей статье в Википедии. Об АК кратко было рассказано в статье «Как совместить логику и семантику в одной алгебраической системе». Там же есть ссылки на публикации с более подробным описанием АК.

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

• она универсальна - позволяет ТОЧНО выразить все (за исключением нуля) конечные целые и рациональные (с любым ненулевым целым числом в знаменателе) числа, а также некоторые классы иррациональных чисел;

• ее использование позволяет сократить вычислительную сложность алгоритма умножения чисел;

• в ней существенно уменьшается объем памяти для записи и хранения многих больших чисел.

Привет, Хабр!

В данной статье сделан обзор на фреймворк планирования движения BMPF.

На данный момент подавляющее большинство средств планирования движения работает по одному и тому же принципу: вся сцена описывается как один робот, после чего выполняется планирование на сетке (чаще всего A*, подробнее можно прочитать здесь).

У такого подхода есть две основных проблемы:

1) планирование на сетке гарантирует допустимость только состояний в её узлах, промежуточные никак не оцениваются и не проверяются.

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

Данный фреймворк решает обе озвученные проблемы. С документацией фреймворка можно ознакомиться здесь.

Привет, Хабр!

Как ты помнишь, в Smart Engines мы разрабатываем томографическое программное обеспечение. Иногда в промышленных и медицинских целях важно заглянуть внутрь окружающих нас вещей, чтобы обнаружить глазом не различимые дефекты детали или же предупредить возникновение заболевания определенного внутреннего органа человека. Нередко на пути восстановления внутренней структуры объектов мы сталкиваемся с множеством трудностей: томограф, используемый для сбора измерений изучаемого объекта, как правило, неидеален, и получаемое изображение внутренности объекта имеет очевидные искажения, двоения, размытия, на нем видны полосообразные или кольцеобразные элементы повышенной или пониженной интенсивности – так называемые артефакты реконструкции объекта. Такие артефакты реконструированного изображения запутывают исследователя и толкают его в пучину заблуждений. Сегодня мы хотели бы рассказать о кольцевых артефактах реконструкции и существующих методах их подавления.

Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования.

Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.

Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «Proof инженер» или «Специалист по формальной верификации». А люди, работающие по этой специальности — есть.

Программное обеспечение, которое прошло формальную верификацию считается надежным. Формальная верификация дает (с математической точностью) гарантии того, что программный код не будет содержать конкретных ошибок, что функции будут вести себя так, как ожидается.

В основе формальной верификации лежат математические методы. Слово «формальный» в названии - это отсылка к математике. Для доказательства утверждений о программном коде используются формальные методы математики: математическая логика, лямбда исчисление, теория категорий, математический анализ, алгоритмы для работы с функциональными и императивными структурами данных.

Инструменты для верификации — это программные средства для доказательства теорем (Coq, Isabelle ...), а также SAT-solvers.

В 70х годах предки формальной верификации — это доказательства простых утверждений о программе (конкретной функции) с помощью ручки и листка бумаги. Сегодня — это (иногда многолетние) исследовательские проекты для конкретного программного обеспечения, вот некоторые из них:

В прошлой части мы рассмотрели базовые понятия в квантовых вычислениях: кубиты, вероятности состояний, измерения.

Квантовые гейты

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

Желание одного студента не сдавать выпускной экзамен привело к появлению вездесущего алгоритма, который сжимает данные, не жертвуя при этом информацией.

Сколько раз при изобретении очередного метода обработки структурированных данных наталкиваешься на мысль о дежавю? Работа со списками файлов, словарями имен, объектными полями, связывание разнотипных данных. В каждом новом более удобном или более быстром переизобретении проглядывается что-то общее, непреходящее. Концептуальное ядро, связующее все возможные производные множества и включающее их в свою орбиту. Что-то чему язык затрудняется сходу подобрать название, а мозг очертить предельные границы. Одновременно всеобъемлющая и при этом неуловимо малая деталь. Абсолютная абстракция. Линейный примитив.

Всем привет! Меня зовут Нурислам (aka tonitaga), и сегодня я бы вам хотел рассказать об Базовых алгоритмах на графах.