Корректность алгоритма решения задачи трехсторонней непересекаемости
Проблема состоит в том, чтобы решить, имеют ли три непустых набора целых чисел, представленные в виде трех массивов A, B и C (списки Python в коде ниже), пустое пересечение.
Я написал следующий код Python, реализующий алгоритм решения этой проблемы:
def disjoint(A, B, C):
"""Solves (?) three-way disjointness problem in n*log(n) time.
"""
A = sorted(A[:])
B = sorted(B[:])
C = sorted(C[:])
i = j = k = 0
while i < len(A) and j < len(B) and k < len(C) and (A[i] != B[j] or B[j] != C[k]):
if A[i] <= B[j] and A[i] <= C[k]:
i += 1
elif B[j] <= A[i] and B[j] <= C[k]:
j += 1
else:
k += 1
if i < len(A) and j < len(B) and k < len(C):
return False
else:
return True
Алгоритм вроде бы правильный (интуитивная идея вроде норм, и в конкретных тестах работает нормально), однако доказать это формально я не могу.
Итак, вопрос: как доказать правильность приведенного выше алгоритма? Что такое хороший рабочий инвариант цикла для доказательства? (Или, если он неверен, контрпример. Обратите внимание, что Python здесь не имеет значения, я мог бы написать его в псевдокоде. Меня интересуют квазиформальные аргументы в пользу правильности этого алгоритма.)
(Я сам пытался привести формальное доказательство; я проверил эту идею на практике, и она, кажется, работает.)
Докажите, указав инвариант цикла: списки до i,j,k не пересекаются (тривиально верно в начале). Затем покажите, что каждая итерация оставляет утверждение истинным.
Вот в чем для меня проблема: я не могу привести убедительный аргумент в пользу того, что если мы знаем, что все списки до (исключая) i, j, k не пересекаются; и условие цикла оценивается как True, тогда после увеличения наименьшего из i, j, k на единицу все списки до (модифицированных) i, j, k по-прежнему не пересекаются. Убедительный (квази)формальный аргумент в пользу того, что это так, до сих пор ускользает от меня.
Ответы 2
В следующем доказательстве используются следующие обозначения:
{X} — множество с одним элементом X,
+ — союз,
* — пересечение.
Пусть непустые множества A,B,C разбиты на подмножества:
A = {A0} + A1, {A0} * A1 = 0
B = {B0} + B1, {B0} * B1 = 0
C = {C0} + C1, {C0} * C1 = 0
где A0,B0,C0 — первые элементы (нижние границы) A,B,C.
{A0} * {B0} != 0 только если A0 == B0 и так далее.
Пересечение A,B,C есть
A * B * C = S0 + Sa + Sb + Sc
S0 = {A0} * {B0} * {C0}
Sa = {A0} * ({B0} * C1 + B1 * {C0} + B1 * C1) + A1 * ({B0} * {C0} + {B0} * C1 + B1 * {C0} + B1 * C1)
Sb = {B0} * ({A0} * C1 + A1 * {C0} + A1 * C1) + B1 * ({A0} * {C0} + {A0} * C1 + A1 * {C0} + A1 * C1)
Sc = {C0} * ({A0} * B1 + A1 * {B0} + A1 * B1) + C1 * ({A0} * {B0} + {A0} * B1 + A1 * {B0} + A1 * B1)
Если S0 != 0, то множества не пересекаются.
Очевидно, что если A0 ≤ B0, то {A0} * B1 == 0 и так далее.
Пусть A0 ≤ B0 и A0 ≤ C0 тогда
Sa = A1 * ({B0} * {C0} + {B0} * C1 + B1 * {C0} + B1 * C1)
Sb = {B0} * (A1 * {C0} + A1 * C1) + B1 * (A1 * {C0} + A1 * C1)
Sc = {C0} * (A1 * {B0} + A1 * B1) + C1 * (A1 * {B0} + A1 * B1)
Поскольку A0 полностью удалено из Sa, Sb и Sc, {A0} также можно вычесть из A, а A * B * C все еще можно использовать для определения непересекаемости.
B0 можно удалить из B в случае B0 ≤ A0 и B0 ≤ C0. И то же самое для C.
Если какое-либо измененное множество стало пустым, то эти множества не пересекаются, поскольку A * B * C == 0. В противном случае требуется следующая итерация.
Алгоритм правильный. Работающий инвариант цикла — Any common element must be >= max(A[i], B[j], C[k]).
Отсюда легко показать, что i, j или k увеличивается только тогда, когда он указывает на слишком маленькое значение, и что инвариант все еще сохраняется после увеличения, поскольку сортировка гарантирует отсутствие возможных общих элементов. между старыми и новыми ценностями.
Как это часто бывает, доказательство корректности позволяет упростить код, поскольку вам не нужно находить наименьший из трех элементов, а достаточно найти тот, который меньше максимального:
def disjoint(A, B, C):
"""Solves (?) three-way disjointness problem in n*log(n) time.
"""
A = sorted(A[:])
B = sorted(B[:])
C = sorted(C[:])
i = j = k = 0
while i < len(A) and j < len(B) and k < len(C):
m = max(A[i], B[j], C[k])
if A[i] < m:
i += 1
elif B[j] < m:
j += 1
elif C[k] < m:
k += 1
else
return False
return True
Спасибо за ваш ответ и хороший инвариант цикла.
Прочитав ваш ответ, я также привел убедительное, хотя и несколько неформальное, доказательство: сначала обратите внимание, что если условие цикла выполнено, то ровно одно из i, j, k будет увеличено на единицу. Если общего элемента нет, то очевидно, что цикл завершается с выходом одного индекса за пределы, и алгоритм правильно решает, что мы имеем трехстороннюю непересекаемость. Теперь предположим, что есть некий общий элемент. Рассмотрим самый маленький из распространенных элементов. В какой-то момент выполнения цикла один из индексов станет индексом наименьшего элемента в одном из
списки. Скажем (блог), что первым, кто добрался до этого общего элемента, является i. Теперь, в последующих итерациях, и благодаря тому, что списки отсортированы, i не будет увеличиваться, а j и k будут увеличиваться до тех пор, пока один из них не достигнет общего элемента в другом списке (поскольку мы перемещаем индекс, не указывающий на самый большой элемент) . Затем оставшийся индекс будет увеличиваться до тех пор, пока не достигнет нашего общего элемента, после чего цикл завершается. Затем алгоритм правильно решает, что списки не являются трехсторонними.
Этот вопрос выглядит знакомым.