Как определить есть ли противоречия в цепочке логических выражений?

Question

[Raynemar]

Есть список из n объектов
Каждый объект обладает значением (некое целое число) и списком свойств ограничивающих его возможное значение через сравнение с другими объектами в списке или сравнение с постоянными значениями
Например:
1. Объект 'a' : a >= 0. a > b. a <= c
2. Объект 'b' : b == f. b < c
3. Объект 'c' : c != f. c < d
4. Объект 'd' : d < e. d > 7
5. Объект 'e' : e < a
6. Объект 'f' : f > 12

Придумать алгоритм, который определит наличие или отсутствие противоречий

Comments

[Максим Гришин]

Ну здесь неравенства сводятся к a<a, то есть система неразрешима. Но если имеется в виду придумать "общий" алгоритм, то да, построение ориентированного графа и поиск в нем циклов, в случае наличия ответ "нет", в случае отсутствия проверка на длину дерева между целыми числами на каждом конце (пример 6<a<b<c<d<9 - в действительных числах совместна, в целых нет).
PS: кто на хабре разучился искать пару скобок < и > в парсере комментов?

Answer 1

[Wataru]

Алгоритм называется "обход в глубину на графе". Работает за линию, все очень быстро. Правда, его придется применить несколько раз.

Все неравенства "==" замените на пару "<=" и ">=".
Добавьте неравенства 1 < 2, 3 < 4 и т.д. для каждой пары соседних на числовой прямой чисел во входных данных

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

Теперь, если в этом графе нет циклов, содержащих белые ребра (строгие неравенства) - то противоречий нет: Все циклы целиком из черных ребер означают, что все вершины имеют одинаковое значение. Можно эти вершины все объединить в одну новую. Раз белые ребра (<) циклов не образуют, то получившийся граф будет ациклическим и можно назначить всем вершинам какие-то числовые значения, удовлетворяющие условиям. Проблема может еще быть, что нет целых решений вроде 1== a < b < c == 2, но это можно потом проверить в топологической сортировке жадно назначая всем вершинам числа. Или противоречия вида 2==3. Тоже решается после получения компонент связности.

Итак, алгоритм: найдите в этом графе компоненты сильной связности. Потом проверьте все ребра. Если белое ребро (строгое неравнество) имеет оба конца в одной и той же компоненте - вы нашли противоречие.

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

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

В конце вы получите для каждой компоненты ее численное значение без каких-либо противоречий.

Comments

[Alexandroppolus]

а что делать для "!=" ?

по идее, это разбивается на ">" или "<", и надо проверять оба варианта по отдельности. Но тогда каждый "!=" удваивает количество раскладов

[Wataru]

Alexandroppolus, неравнства я не заметил. Можно в конце проверить вместе с ребрами в компоненте. Если неравно в одной компоненте - противоречие. Если идет в большую компоненту, пока пропускаем. Если в меньшую компоненту, и пока оценка минимального числа равна, увеличим оценку на 1

[Alexandroppolus]

Wataru, да, так вроде норм.

Ещё я бы не менял "==" на пару "<=" и ">=", а сразу схлопывал две вершины в одну (при этом ребра "поглощаемой" вершины переходят на "основную"). При схлопывании "X === число" основной вершиной всегда делать число

[Wataru]

Alexandroppolus, я думал об этом, но это не нужно. Все равно надо обрабатывать случай циклов из <=. Отдельно равенства обрабатывать - лишний код будет.

Answer 2

[mayton2019]

Можно попробовать на Prolog написать. Правила (rules) известны. А в качестве утверждений - просто
проверить что существуют ли целые числа которые удовлетворяют всем rules.

Answer 3

[Griboks]

Полный ленивый перебор. Разумеется, это сработает только на небольшом объёме данных.

Для большого, боюсь, придётся решать систему логических уравнений.