This is an example program that finds the probability of drawing a Poker pair from a deck. There's a matching
example that shows how to do this in a straight forward manner. Here we have a comparison
of the two approaches.
This example approaches the problem differently by using a more compact representation of each drawn card.
Instead of assigning each card an assumption we use 4 assumptions to represent a rank (note 2^4=16),
and a further two assumptions to represent the suit. Note there's a total of 4 suits and 13 ranks giving us the 52 cards.
This way, we get 6 assumptions (note 2^6=64 > 52) to represent a drawn card from a deck. This way of drawing cards means
that an assignment of assumptions corresponds to a single card drawn at a time (ie. avoids contradictions).
The remaining 14 cards in a deck out of 64 are marked as contradictory - hence out of consideration.
We define a set of 6 assumption for each draw. That gives us 5 * N draws assumptions overall to represent a draw of N cards
from a standard deck.
We mark that when a card is drawn once the other draws become contradictory. Any assignment of assumptions corresponds
to a draw - and that gives us the final requirement that a card has to be drawn in a draw.
Here are some metrics between this example and the naive version. Times are taken on a modest laptop (as of 2017) and timings
are here to give a rough idea and so not very methodically captured:
NUM_RANKS NUM_SUITS NUM_DRAWS #assumptions ~#scenarios ~duration (sec)
13 2 3 78 3e23 900
13 4 2 104 2e31 186
8 4 2 64 2e19 21
13 4 3 156 9e46 57000
13 4 4 260 2e78 -
13 4 5 260 2e78 -
13 2 3 15 3e4 3
13 4 2 12 4e3 2
8 4 2 10 1e3 1
13 4 3 18 3e5 43
13 4 4 24 2e7 7000
13 4 5 30 1e9 -
It can be seen that the
runs much faster, and there's a non-linear relation between the runtime
and the number of assumptions even though more assumptions generally cause slower runs. Most of the time spent here
tends to be during the symbolic QS finding which is an area improvement in OpenPAS.
Unfortunately neither version can fully handle the 5 draws case which is arguably the most interesting/useful one. Further OpenPAS
improvements should make this possible (e.g. use of a BDD based symbolic engine).
The idea with these examples is that you run it to generate an .ops file, and then can continue playing with these PAS instances
. You can modify the variables NUM_DRAWS, NUM_RANKS, and NUM_SUITS to investigate different configurations.
It may be instructive to reduce these numbers to e.g. 2/2/2 and perform a "scenarios" analysis in PASC to get a close look into
how PAS works under the cover.
When run, the program continues to attempt to calculate the dsp for "got_pair" which is the Poker pair proposition. This is
to give an idea about how to programmatically perform numerical computations.