Ограничения компаратора

Question

Знаете ли вы инструмент, который я мог бы использовать для сравнения ограничений (не только математических)? Это проще объяснить на примерах:

A) Простой пример

C1: x < 0 && y * y < x
C2: x < 0 && y * y < x - 1

Я хочу знать, сильнее ли С2, чем С1, и так оно и есть. Это означает, что (x, y) из C2 также находятся в C1.

Б) Сложный пример

C1: x > 0 && y > 0
C2: x > 0

C2 слабее, чем C1, потому что не содержит ограничений на y.

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

Спасибо

Answer 1

Вы пытаетесь решить, относится ли ограничение C1 к C2 (имеется в виду, что невозможно найти набор значений, которые удовлетворяют C1 и не удовлетворяют C2 -> C2, верно во всех сценариях, в которых C1 верно, но, возможно, нет наоборот)? Когда C1 включает C2, то C2 можно удалить, поскольку это не добавляет семантики к проблеме.

Если это так, я рекомендую вам использовать для этого CSP-решатель. Это проще, чем кажется. Например, решатель Eclipse CSP (здесь Eclipse не ссылается на платформу IDE, так как решатель имеет одно и то же имя) может быть легко вызван из вашей Java-программы через четко определенный API, поэтому вы можете просто отправить проблему решателю и посмотрите, какое ограничение слабее

Answer 2

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