Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>First, to correct a few things that are just blatently wrong in your question:</p> <ul> <li><p><code>solve</code> solves for algebraic expressions. <code>solve(expr, x)</code> solves the equation expr = 0 for <code>x</code>. </p></li> <li><p><code>solve(x | y = False)</code> and so on are invalid syntax. You cannot use <code>=</code> to mean equality in Python. See <a href="http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signs" rel="nofollow noreferrer">http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signs</a> (and I recommend reading the rest of that tutorial as well). </p></li> <li><p>As I mentioned in the answer to <a href="https://stackoverflow.com/questions/19703284/boolean-operation-with-symbol-in-sympy">another</a> question, <code>Symbol('y', bool=True)</code> does nothing. <code>Symbol('x', something=True)</code> sets the <code>is_something</code> assumption on <code>x</code>, but <code>bool</code> is not a recognized assumption by any part of SymPy. Just use regular <code>Symbol('x')</code> for boolean expressions.</p></li> </ul> <p>As some commenters noted, what you want is <code>satisfiable</code>, which implements a SAT solver. <code>satisfiable(expr)</code> tells you if <code>expr</code> is satisfiable, that is, if there are values for the variables in <code>expr</code> that make it true. If it is satisfiable, it returns a mapping of such values (called a "model"). If no such mapping exists, i.e., <code>expr</code> is a contradiction, it returns <code>False</code>. </p> <p>Therefore, <code>satisfiable(expr)</code> is the same as solving for <code>expr = True</code>. If you want to solve for <code>expr = False</code>, you should use <code>satisfiable(~expr)</code> (<code>~</code> in SymPy means not). </p> <pre><code>In [5]: satisfiable(x &amp; y) Out[5]: {x: True, y: True} In [6]: satisfiable(~(x | y)) Out[6]: {x: False, y: False} In [7]: satisfiable(x &amp; y &amp; z) Out[7]: {x: True, y: True, z: True} </code></pre> <p>Finally, note that <code>satisfiable</code> only returns one solution, because in general this is all you want, whereas finding all the solutions in general is extremely expensive, as there could be as many as <code>2**n</code> of them, where <code>n</code> is the number of variables in your expression. </p> <p>If however, you want to find all of them, the usual trick is to append your original expression with <code>~E</code>, where <code>E</code> is the conjunction of the previous solution. So for example, </p> <pre><code>In [8]: satisfiable(x ^ y) Out[8]: {x: True, y: False} In [9]: satisfiable((x ^ y) &amp; ~(x &amp; ~y)) Out[9]: {x: False, y: True} </code></pre> <p>The <code>&amp; ~(x &amp; ~y)</code> means that you don't want a solution where <code>x</code> is true and <code>y</code> is false (think of <code>&amp;</code> as adding extra conditions on your solution). Iterating this way, you can generate all solutions. </p>
    singulars
    1. This table or related slice is empty.
    1. POSolving Symbolic Boolean variables in Python
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USCommunity
    1. USasmeurer
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POSolving Symbolic Boolean variables in Python
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COAnd if `satisfiable` ends up being too slow for you, check out other SAT solvers which are written in C. `picosat` for instance may be useful. It will require you to formulate your problem in a more rudimentary way (so-called DIMACS cnf form), but such solvers will return a solution almost instantly even for quite large problems.
      singulars
      1. PO
      1. USasmeurer
    2. COAnd I should mention that `picosat` has Python bindings, called `pycosat`.
      singulars
      1. PO
      1. USasmeurer
    3. COGreat! One thing I would like to add, I found that only one solution is sufficient for my purpose.
      singulars
      1. PO
      1. USpushpen.paul
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload