с учетом ряда условий, алгоритмически определить, что только одно может быть истинным.
Учитывая набор из двух или более логических условий, можно ли алгоритмически определить, что ровно ОДНО из них будет иметь значение ИСТИНА? Например:
# this should pass, since for every X, only one condition is taken
cond 1: (X >= 1.0)
cond 2: (X < 1.0)
# this should fail
cond 1: (X < 1.0)
cond 2: (X > 2.0)
# this should also fail, since X=1.0 would meet both conditions
cond 1: (X < 2.0)
cond 2: (X > 0.0)
# there may be more than one variable involved
cond 1: (X >= 1.0 && Y >= 0)
cond 2: (X < 1.0 && Y <= -1)
Эти условия генерируются из предметно-ориентированного языка и используются для определения следующего пути выполнения. т. е. пользователи составляют условие для каждой опции, когда дерево выполнения разделяется на несколько путей, а условие, которое оценивается как истинное, определяет путь, который должен быть выбран. Для того чтобы моделирование было действительным, это должен быть только один возможный путь, который может быть выбран для любых заданных значений.
В настоящее время Я оцениваю эти условия во время выполнения и выкидываю истерику, если более одного (или ни одного) из них истинны.
Я хотел бы иметь возможность проверять ошибочные условия на этапе синтаксического анализа (от языка домена до компилируемого исходного кода). Является ли это возможным? Как можно провести проверку условий?
Обновление
Что касается того, что может быть включено в условия, сфера применения на практике довольно широка. Все это возможные условия:
X> = Y && YX.within_radius (0.4)X IN some_arrayX * Y
окончательное обновление
Это делает кажется, что решение, которое охватывает все возможные условия, невозможно (или, по крайней мере, учитывая мои ограниченные знания, невозможно в течение времени, отведенного для решения проблемы). Я вернусь к этому когда-нибудь, но пока принимаю ответ, который выдвинул меня вперед.
4 ответа
РЕДАКТИРОВАТЬ: Я повторю, потому что кажется, что другие ответы предполагают множество вещей, которые с тех пор были подтверждены:
Если вы можете указать свои условия (и ограничение, которое только одно верно) в терминах арифметики Пресбургера , то вы можете написать процедуру принятия решения для статической проверки этого свойства. Это кажется вполне достижимым из приведенных выше примеров.
Подход «тупого инструмента» состоит в том, чтобы в основном взаимодействовать с чем-то вроде автоматического доказательства теорем или решателя SMT (где вы в основном пытаетесь доказать отрицание утверждения «существует некоторое значение x, которое удовлетворяет ограничению constraint1 XOR2») ).Я программно взаимодействовал с CVC3 раньше и нашел его довольно удобным для работы, но я понимаю, что другие решатели SMT превзошли его.
Я думаю, что все остальное, что вы делаете для решения этой проблемы, в конечном итоге приблизится к некоторой реализации инструментов, которые я предложил. В зависимости от того, как конкретно заданы ваши ограничения, вам, возможно, удастся реализовать какую-то процедуру принятия решения для чего-то вроде арифметики Пресбургера .
В общем, нет. Но если вы действительно спрашиваете, возможно ли это при условиях, составленных из логических комбинаций неравенств на конечном наборе независимых целочисленных переменных с константами, тогда есть надежда. Вы можете полностью проверить, переставив переменные с константами, которые фигурируют в ваших неравенствах (и +1 и -1 этих констант), и убедившись, что количество условий, которые выполняются, всегда равно 1.
Если вы хотите выяснить, выполняется ли только одно условие (из двух или более возможных), может быть полезно обратиться к этому вопросу xor на SO: xor-of- трехзначность . Исходя непосредственно из его ответа:
(a ^ b ^ c) && !(a && b && c)
В вашем случае:
(cond 1 ^ cond 2 ^ cond 3) && !(cond 1 && cond 2 && cond 3)
Существует также общее решение, при котором вы увеличиваете счет каждый раз, когда выполняется какое-либо условие, а затем сравниваете счет с 1 после того, как все условия были проверены.
Являются ли ваши строительные блоки условиями просто
- целочисленной переменной,
- оператором сравнения из (<, <=,>,> =),
- чисел ( предположим целые числа)?
И окончательные условия строятся из них с помощью && и ||?
Можно ли предположить, что все целочисленные переменные независимы?
В этих условиях я бы предположил, что это может быть проверено алгоритмически . Я бы поместил все допустимые диапазоны для каждой переменной в структуру данных и проверял пересечения.
РЕДАКТИРОВАТЬ: Поскольку это не похоже на случай, лучшим решением, вероятно, было бы сгруппировать различные типы условий, чтобы условия в каждой группе можно было статически сравнивать друг с другом. Тип условий, принятых мной из вашего первого описания, будет лишь одной из этих групп.