Message Boards Message Boards

1
|
5100 Views
|
6 Replies
|
1 Total Likes
View groups...
Share
Share this post:
GROUPS:

Are the logical expressions returned by Reduce always satisfiable ?

Hello everyone,

I am trying to solve conjunctions of linear equations together with linear inequalities. As I am looking for a complete solution, and due to the inequalities, I know that the function to use is Reduce.

Reduce expresses the complete solution in a logical expression. When the logical expression is simple enough, we can manually verify that it is satisfiable and thus that solution(s) exist(s). But as we can hardly perform such manual verification when the logical expression begins to be too long, the following question arises : when Reduce returns a logical expression different from True or False, is that logical expression always satisfiable ? The fact that I am dealing with linear systems might help.

Thanks in advance.

6 Replies

Are the logical expressions returned by Reduce always satisfiable ?

POSTED BY: Simon Cadrin

If there's no solution, Reduce will return False.

In[6]:= eqs = {2 x + 3 y <= 5, x - 2 y >= 1, 1 <= x <= 10, 
   1 <= y <= 10};

In[7]:= res = Reduce[eqs, {x, y}]

Out[7]= False
POSTED BY: Frank Kampas

Are the logical expressions returned by Reduce always satisfiable ?

POSTED BY: Simon Cadrin

My wonder is when Reduce returns an answer different from True or False. For example, when Reduce returns something like this : enter image description here

Can such expressions returned by Reduce be unsatisfiable ? Or are they always satisfiable ?

If I understand your question correctly, the results are always satisfiable. If the input to Reduce is inconsistent, it returns False.

POSTED BY: Frank Kampas

Thank you

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract