Решение проблем удовлетворения ограничений в Sympy

Я пытаюсь решить несколько простых задач логической выполнимости в Sympy. Здесь я попытался решить ограничение, содержащее логический оператор Or:

from sympy import *
a,b = symbols("a b")

print(solve(Or(Eq(3, b*2), Eq(3, b*3))))
# In other words: (3 equals b*2) or (3 equals b*3)
# [1,3/2] was the answer that I expected

Удивительно, но вместо этого возникает ошибка:

TypeError: unsupported operand type(s) for -: 'Or' and 'int'

Я могу обойти эту проблему с помощью Piecewise, но это гораздо более подробный вариант:

from sympy import *
a,b = symbols("a b")
print(solve(Piecewise((Eq(3, b*2),Eq(3, b*2)), (Eq(3, b*3),Eq(3, b*3)))))
#prints [1,3/2], as expected

К сожалению, этот обходной путь не удается, когда я пытаюсь найти две переменные вместо одной:

from sympy import *
a,b = symbols("a b")

print(solve([Eq(a,3+b),Piecewise((Eq(b,3),Eq(b,3)), (Eq(b,4),Eq(b,4)))]))
#AttributeError: 'BooleanTrue' object has no attribute 'n'

Есть ли более надежный способ решения подобных ограничений в Sympy?


sympy constraint-programming smt
person Anderson Green    schedule 29.11.2016    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Чтобы расширить ответ zaq, SymPy не распознает логические операторы в solve, но вы можете использовать тот факт, что

a*b = 0

эквивалентно

a = 0 OR b = 0

То есть умножьте два уравнения

solve((3 - 2*b)*(3 - 3*b), b)

В качестве дополнительного примечания, если вы хотите использовать И вместо ИЛИ, вы можете решить для системы. То есть,

solve([eq1, eq2])

эквивалентно решению

eq1 = 0 AND eq2 = 0
person asmeurer    schedule 01.12.2016
comment
Этот метод иногда работает, когда формула записана в нормальной конъюнктивной форме, но не всегда дать все возможные решения. Например: в (y-x = 1) AND ((x = 1) OR (1/(1-x) = 1/2)) одно из уравнений имеет решение, в то время как другое уравнение не определено, поэтому в этом случае оно не даст всех решений. - person Anderson Green; 26.10.2020
comment
@AndersonGreen вы можете использовать solve(check=False), чтобы отключить проверки того, что решение делает знаменатель равным нулю. solve((1 - x)*(1/(1 - x) - S(1)/2), x, check=False) дает [-1, 1]. - person asmeurer; 28.10.2020

arrow_upward
4
arrow_downward

Каждое уравнение можно выразить как нечто, приравниваемое к 0. Например, 3-2 * b = 0 вместо 3 = 2 * b. (Предполагается, что в Sympy вам даже не нужно писать часть =0.) Затем вы можете просто перемножить уравнения, чтобы выразить логику ИЛИ:

>>> from sympy import *
>>> a,b = symbols("a b")
>>> solve((3-b*2)*(3-b*3))
[1, 3/2]
>>> solve([a-3-b, (3-b*2)*(3-b*3)])
[{b: 1, a: 4}, {b: 3/2, a: 9/2}]
person Community    schedule 29.11.2016