Library for creating circuits that encode discrete distributions.
Project description
pyaigercoins
Library for creating circuits that encode discrete distributions and Markov Decision Processes. The name comes from the random bit model of drawing from discrete distributions using coin flips.
Table of Contents
Install
To install this library run:
$ pip install pyaigercoins
Note that to actually compute probabilities, one needs to install with the bdd option.
$ pip install pyaigercoins[bdd]
For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:
$ poetry install
Usage
Note this tutorial assumes pyaigerbdd
has been installed (see the
Install section).
Biased Coins
We start by encoding a biased coin and computing its bias. The primary
entrypoint for modeling coins is the coin
function.
from fractions import Fraction import aiger_coins bias = Fraction(1, 3) coin1 = aiger_coins.coin(bias) coin2 = aiger_coins.coin((1, 3)) # or just use a tuple. assert coin1.prob() == coin2.prob() == prob
Distributions on discrete sets
We now illustrate how to create a set of mutually exclusive coins that represent distribution over a finite set. For example, a biased three sided dice can be 1hot encoded with:
dice = aiger_coins.dist([1, 3, 2], name='x') dice = aiger_coins.dist([(1, 6), (3, 6), (2, 6)], name='x') # equivalent dice = aiger_coins.dist([Fraction(1, 6), Fraction(3, 6), Fraction(2, 6)], name='x') # equivalent print(dice.freqs()) # (Fraction(1, 6), Fraction(1, 2), Fraction(1, 3))
Letting, ⚀ = dice[0]
, ⚁ = dice[1]
, ⚂ = dice[2]
,
one, two, three = dice[0], dice[1], dice[2]
We can ask the probability of drawing an element of {⚀, ⚁}
with:
assert (one  two).prob() == Fraction(2, 3) assert (~three).prob() == Fraction(2, 3)
Distributions and Coins
Distribution
s and Coin
s are really just wrappers around two
aiger_bv.UnsignedBVExpr
objects stored in the expr
and valid
attributes.
The attributes expr
and valid
encode an expression over fair coin
flips and which coin flips are "valid" respectively. Coins is a
special type of Distribution
where the expression is a predicate
(e.g. has one output).
Note that accessing the ith element of a Distribution
results in a
Coin
encoding the probability of drawing that element.
Manipulating Distributions
In general Distribution
s can me manipulated by manipulating the
.expr
attribution to reinterpret the coin flips or manipulating
.valid
to condition on different coin flip outcomes.
Out of the box Distribution
s support a small number of operations:
+, <, <=, >=, >, ==, !=, ~, , &, ^, .concat
, which they inherit
from aiger_bv.UnsignedBVExpr
. When using the same .valid
predicate
(same coin flips), these operations only manipulate the .expr
attribute.
More generally, one can use the apply
method to apply an arbitrary
function to the .expr
attribute. For example, using the dice from
before:
dice2 = dice.apply(lambda expr: ~expr[2]) assert dice2[0].freqs() == Fraction(2, 3)
One can also change the assumptions made on the coin flips by using
the condition method, for example, suppose we condition on the coin
flips never being all False
. This changes the distribution
as follows:
coins = dice.coins # Bitvector Expression of coin variables. dice3 = dice.condition(coins != 0) print(dice3.freqs()) # [Fraction(0, 5), Fraction(3, 5), Fraction(2, 5)]
Binomial Distributions
As a convenience, pyaigercoins
also supports encoding Binomial
distributions.
x = binomial(3) print(x.freqs()) # (Fraction(1, 8), Fraction(3, 8), Fraction(3, 8), Fraction(1, 8))
Markov Decision Processes and Probablistic Circuits
aiger_coins
also supports modeling Probablistic Circuits, Markov
Decision Process (MDPs), and Markov Chains (MDPs with no inputs).
Internally, the MDP
object is simply an AIGBV
bitvector circuit
with some inputs annotated with distributions over their inputs.
The primary entropy point to modeling a Markov Decision Process is
the circ2mdp
function.
from aiger_bv import atom from aiger_coins import circ2mdp x = atom(3, 'x', signed=False) y = atom(3, 'y', signed=False) expr = (x & y).with_output('x&y') mdp1 = circ2mdp(expr) mdp1 = circ2mdp(expr.aigbv) # equivalent
Composition
MDP
can be composed using an API analogous to aiger_bv.AIGBV
and
aiger.AIG
sequential circuits. In addition, MDP
support being feed
actions from a distribution via sequential composition.
# Put a distribution over the y input. dist = aiger_coins.dist((0, 1, 2), name='y') mdp2 = dist >> mdp1 mdp2 = mdp1 << dist # equivalent mdp2 = circ2mdp(expr, {'y': dist}) # equivalent assert mdp1.inputs == {'x', 'y'} assert mdp2.inputs == {'x'} mdp3 = mdp2  circ2mdp(aiger_bv.identity_gate(4, 'z')) assert mdp3.inputs == {'x', 'z'} assert mdp3.outputs == {'x&y', 'z'} mdp4 = mdp3.feedback(inputs=['z'], outputs=['x&y'], keep_outputs=True) assert mdp4.inputs == {'x'} assert mdp4.outputs == {'x&y', 'z'}
Extracting Circuit
One can transform an MDP
into an AIG
or AIGBV
object using
.aig
and .aigbv
attributes. This adds as the coinflips explicitly
as inputs and also adds a special output ##valid
that monitors if
the sequence of inputs and coin flips was valid.
assert mdp.aigbv.outputs == mdp.outputs  {'##valid'} assert '##valid[0]' in mdp.aig.outputs
Encoding and Decoding Traces
Often times, one is interested in analyzing traces, sequences of states and actions, through a Markov Decision Process.
In order to map this to an execution of an MDP
object, one needs to
find a sequence of coin flip inputs such that feeding the actions and
the coin flip inputs into the circuit generated by MDP.aigbv
.
This (and its inverse) can be done via the MDP.encode_trc
and
MDP.decode_trc
methods.
For example, consider the simple MDP modeled by:
from aiger_bv import atom from aiger_coins import circ2mdp action = atom(1, 'action', signed=False) x_prev = atom(1, 'x_prev', signed=False) c = atom(1, 'c', signed=False) x_next = (x_prev & c & action).with_output('x_next') sys = circ2mdp(x_next).feedback( keep_outputs=True, inputs=['x_prev'], outputs=['x_next'], initials=[(True,)], ) sys <<= coin((1, 2), name='c') assert sys.inputs == {'action'} assert sys.outputs == {'x_next'}
We can encode and decode traces into this model as follows:
# Encoding and Decoding
sys_actions = 3*[{'action': (True,)}]
states = 3*[{out: (True,)}]
actions = sys.encode_trc(sys_actions, states)
assert not any(v['c'][0] for v in actions)
sys_actions2, states2 = sys.decode_trc(actions)
assert sys_actions2 == sys_actions
assert states2 == states
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Filename, size  File type  Python version  Upload date  Hashes 

Filename, size py_aiger_coins1.2.1py3noneany.whl (11.7 kB)  File type Wheel  Python version py3  Upload date  Hashes View hashes 
Filename, size pyaigercoins1.2.1.tar.gz (13.3 kB)  File type Source  Python version None  Upload date  Hashes View hashes 
Hashes for py_aiger_coins1.2.1py3noneany.whl
Algorithm  Hash digest  

SHA256  799f7b92c4c2836888da69e56000f7fa6c9a6a00174c018a3125157f2e67148e 

MD5  303cc96e5717c6d41233940893faa59e 

BLAKE2256  a95ddd511e9ebb4ab7ffdbe5c9f3c9e413d5fcf4daa7a5c022b8e61be82db45e 