CODEWITHSUNDEEP
sympy
rodie9k
rodie9k

Reputation: 111

Sympy check satisfiability of statement involving symbols

I have a program that generates logical statements involving symbols, like conds below

import sympy
x, y = sympy.symbols('x,y')
conds = sympy.Eq(x+y,-1) & (x>1) & (y>2)

I would like to check if they're satisfiable (if there exist x,y meeting the conditions). In general, how can I reduce logical statements involving symbols?

sympy.solve([sympy.Eq(x+y,1), x>1, y>2]) gives a NotImplementedError and the inequality solvers can only handle one variable IIRC.

I'd appreciate any help with this.

Upvotes: 1

Views: 280

Answers (3)

Tilo RC
Tilo RC

Reputation: 13

You can use satisfiable() with the use_lra_theory=True parameter to check the satisfiability of any boolean formula involving linear real inequalities.

>>> from sympy import symbols, Eq
>>> from sympy.logic.inference import satisfiable
>>> 
>>> x, y = symbols('x y')
>>> conds = Eq(x + y, -1) & (x > 1) & (y > 2)
>>> 
>>> satisfiable(conds, use_lra_theory=True)
False
>>>
>>> conds = ((x > 0) | (x < 0)) & Eq(x,0)
>>> satisfiable(conds, use_lra_theory=True)
False

Upvotes: 0

smichr
smichr

Reputation: 19029

A new addition to SymPy is the simplex solver (full disclosure I'm a major author to it PR).

You can pass this equation list to lpmin with an objective of 0 to see if the system is feasible or not

>>> from sympy import *
>>> from sympy.abc import x, y
>>> lpmin(0,(Eq(x+y,1), x>=1, y>=2))
Traceback (most recent call last):
  ...
sympy.solvers.simplex.InfeasibleLPError:
The constraint set is empty!

# change Eq rhs from 1 to 3

>>> lpmin(0,(Eq(x+y,3), x>=1, y>=2))
(0, {x: 1, y: 2})

The first case is infeasible and the second is feasible (and a solution is offered). You must replace < and > with their non-strict counterparts.

Upvotes: 1

Oscar Benjamin
Oscar Benjamin

Reputation: 14480

I'm not sure exactly when this will or won't work (the problem is undecidable in full generality) but SymPy has a function reduce_inequalities that does work for the example shown:

In [8]: reduce_inequalities(conds)
Out[8]: False

Upvotes: 2

Related Questions