26
SatisfiableQ has three methods:
"BDD": converts the expression to a BDD (binary decision diagram),
"SAT": uses the Minisat library,
"TREE": a branch-and-bound method based on the expression tree.
SatisfiabilityCount counts instances by converting the expression to a BDD, so its timing should be close to SatisfiableQ with the "BDD" method (counting ...
19
You can enter the logic formulations into Mathematica like this — Copy & paste the following code, and you can see the symbols.
p = a \[Equivalent] ((a \[And]
b \[And] \[Not] c) \[Or] (a \[And] \[Not] b \[And]
c) \[Or] (\[Not] a \[And] b \[And] c));
q = b \[Equivalent] (b \[And] c);
r = c \[Equivalent] (\[Not] a \[Or] \[Not] b);
We ...
17
The Wolfram Language and Mathematica 10 (available now on the Raspberry Pi) have new functions — AnyTrue, AllTrue, NoneTrue — which take a predicate and test any/all/none on the input list. For example:
AnyTrue[Range@5, EvenQ]
(* True *)
AllTrue[{True, False, False}, TrueQ] (* or Identity in place of TrueQ *)
(* False *)
These functions can also be turned ...
13
You want to complement bits based on a given length. Easy enough.
complementBits[bits_Integer, len_Integer] /; bits >= 0 && len >= 0 :=
BitXor[bits, 2^len - 1]
(If you really want to compliment them, tell them the size is much too big for them..)
Quick test.
complementBits[43, 8]
(* Out[237]= 212 *)
Getting back to the question at hand, ...
12
You can use And and still get what you want:
x := 1
If[And @@ {True, False, True, False, (x := 2; True)}, Print["Yes"], Print["No"]];
x
(* No
2 *)
What happens is that the List and its arguments are evaluated before And is applied to it, hence setting the value of x.
11
This answer is a modification of my answer given in the discussion Creating Identification/Classification trees.
With this solution I am trying to achieve the simplification by using the impurity function applied to the data (the truth table in this case).
Make the truth table from the linked Wikipedia article (Binary Decision Diagram):
truthTable = {{0, ...
10
v1 = RandomChoice[{-1, 1}, 100];
v2 = RandomChoice[{-1, 1}, 100];
vL = UnitStep[v1];
vL*v1 + (1 - vL)*v2
Using PatoCriollo's comparison (and now updated to include rasher and Mr. Wizard's methods):
n = 10^6;
v1 = RandomChoice[{-1, 1}, n];
v2 = RandomChoice[{-1, 1}, n];
(bp = Boole[Positive[v1]];
test1 = bp v1 + (1 - bp) v2); // Timing
test2 = With[{c = ...
10
BooleanMinimize[BooleanFunction[table]]
(* (#1 && ! #2) || (#1 && ! #3) || (#1 && ! #4) || (! #1 && #2 && #3 && #4) & *)
Note in the documentation how 1/0 vs True/False are treated here, massage as needed.
Quick verification:
bf = BooleanFunction[table];
Rule @@@ Transpose[{table[[All, 1]],
bf[...
9
The problem of finding the variable order that minimizes the number of nodes in a given reduced ordered binary decision diagram is NP-hard. So, it is typically not used very much. It is implemented in CUDD as CUDD_REORDER_EXACT.
Rudell's sifting is the algorithm most frequently used. In both a brute force computation of the optimal order, as well as sifting,...
9
Speed here is hindered by the fact that True/False is not a packable type in Mathematica, although I personally think it should be.
If it is possible to reformulate your problem to use 1/0 instead, which can be packed, the methods already provided (Pick and SparseArray) each become much faster.
You can convert your data using With faster than using Boole, ...
8
This happens because Simplify converts the expression to a BooleanFunction representation. Checking the documentation for BooleanFunction you find that:
Elements of both inputs and outputs can be specified either as True
and False or as 1 and 0.
8
It seems I misunderstood the question. Here's an update, which is a considerable improvement, too. It relies on Implies[x, y] being equivalent to Boole[x] (1 - Boole[y]) == 0.
falsePattern = Table[False, {15}, {15}];
truePattern = Table[True, {15}, {15}];
SeedRandom[1];
randomPattern = RandomChoice[{True, False}, {15, 15}];
impliesPosition[board_, ...
8
In addition to HoldAll as highlighted by Pinguin Dirk the other component of the behavior is that And directly returns single arguments:
And[73]
73
Combined, And[check] spits out check which at the top level evaluates to Sequence[True, . . .].
One problem with your method for checking the matrix is that it does not short-circuit on a non-numeric value, ...
8
As in the comments above, we see that the HoldAll attribute is causing the "problem".
Note that if we unset HoldAll it works:
Unprotect@And;
ClearAttributes[And, HoldAll];
Protect@And;
Then:
And[check]
True
EDIT: based on Oleksandr R.'s comment, I must stress that I showed this only to illustrate the "problem". It is not a good idea to unset HoldAll ...
8
In version 10, the new geometric computation functionality supports this. It operates with region objects. Many graphics primitives, including Disk and Rectangle can be used as regions.
Boolean operations include RegionUnion, RegionIntersect, RegionDifference, RegionSymmetricDifference and BooleanRegion.
Example:
RegionPlot[RegionIntersection[Rectangle[]...
8
If I'm not mistaken you should be happy to use Array:
Array[x, 10, 0, And]
x[0] && x[1] && x[2] && x[3] && x[4] && x[5] && x[6] && x[7] && x[8] && x[9]
It works on V9, don't know if for previous versions too.
8
EDIT: This method really just optimizes, and visualizes binary decision trees, not general binary decision diagrams. I answered a question - sadly not one that was asked! :)
"If and constants" ("IF") form of BooleanConvert seems to be sensitive to order of boolean variables; it always builds the tree starting from the first appearing in the description of a ...
8
Distribute[list, List]
giving
{{a, b, c, f, g}, {a, b, c, f, h}, {a, b, d, f, g}, {a, b, d, f, h}}
8
r1 = 40; r2 = 25;
R = RegionUnion[Ball[{0, 0, 0}, r1],
Cylinder[{{Sqrt[r1^2 - r2^2], 0, 0}, {r1, 0, 0}}, r2]];
R // Volume
250/3 (812 + 39 Sqrt[39]) π
Graphics3D[{{Opacity[0.5], Red, Ball[{0, 0, 0}, r1]}, {Opacity[0.5],
Blue, Cylinder[{{Sqrt[r1^2 - r2^2], 0, 0}, {r1, 0, 0}}, r2]}}]
Volume of the blue solid:
Volume[R] - Volume[Ball[{0, 0, 0}, r1]...
8
Boole@Positive[a-b]
{{0, 1, 0}, {1, 0, 1}, {0, 1, 0}}
1-UnitStep[b-a]
{{0, 1, 0}, {1, 0, 1}, {0, 1, 0}}
8
This is what you want ?
StringJoin[Riffle[Partition[Characters[#], 2], "&&"]] & /@ {"x1x2",
"x1", "x1x2x3", "x3", "x4", "x1x2x3x4"}
(* Out: {"x1&&x2", "x1", "x1&&x2&&x3", "x3", "x4", "x1&&x2&&x3&&x4"} *)
8
lst = {"x1x2", "x1", "x1x2x3", "x3", "x4", "x1x2x3x4"};
You can use a combination of StringRiffle and StringPartition
StringRiffle[StringPartition[#, 2], "&&"] & /@ lst
{"x1&&x2", "x1", "x1&&x2&&x3", "x3", "x4", "x1&&x2&&x3&&x4"}
Alternatively, you can use StringReplace:
StringReplace[lst, ...
7
One straightforward way to negate vectors is to use the full form of !, which it Not
q = {True, True, False};
Not /@ q
{False, False, True}
or equivalently Map[Not, q].
7
String matching works a little better. Think of each row in the board as a string on the alphabet {"0", "1"}. The "pattern" is a set of instructions to look for particular configurations of "0" on the board, because a presence of a "1" in the pattern is no restriction at all and a "0" in the pattern means there must be a corresponding "0" on the board. ...
7
You can simply do:
{#, #2} -> #3 & @@@ {{0, 0, 0}, {0, 1, 1}, {1, 0, 1}, {1, 1, 1}}
{{0, 0} -> 0, {0, 1} -> 1, {1, 0} -> 1, {1, 1} -> 1}
7
This sort of thing can be recast as a quantifier elimination problem, as below. Quantify the variables you want to remove, set conditions on them as needed, and use Resolve to do the elimination step. A postprocessing step of BooleanMinimize might be needed (not in the examples below though).
Resolve[Exists[p, p == True, p \[Xor] q]]
(* Out[324]= ! q *)
...
7
As said in comments, that's an efficient way of generating combinations. If you want to do something with them, BooleanTable is pretty neat:
TableForm[
BooleanTable[{{a, b, c}, And[a, b, c], Or[a, b, c], Xor[a, b, c], Xnor[a, b, c]}, {a, b, c}],
TableHeadings -> {None, {"Vars", "And", "Or", "Xor", "Xnor"}}]
7
Posting this here as community wiki because we answers should not stay only as comments.
You have many options
Using Resolve and ForAll
Resolve[ForAll[x, x > 0, Abs[x] == x]]
Using Refine
Assuming[x > 0, TrueQ[Refine[Abs[x] == x]]]
But assumptions can be placed inside Refine, as in
Refine[Abs[x] == x, x > 0]
Using Simplify
Simplify[Abs[x] =...
7
BitOr[{0, 1, 0, 1, 1}, {1, 1, 0, 1, 1}]
$\ ${1, 1, 0, 1, 1}
BitAnd[{1, 1, 0, 0, 0}, {1, 1, 0, 1, 1}]
$\ ${1, 1, 0, 0, 0}
{1, 1, 0, 0, 0} ~BitAnd~ ({0, 1, 0, 1, 1} ~BitOr~ {1, 1, 0, 1, 1})
$\ ${1, 1, 0, 0, 0}
Only top voted, non community-wiki answers of a minimum length are eligible
