{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"\n# Circuits\n\nConvert a Boolean circuit to an equivalent Boolean formula.\n\nA Boolean circuit can be exponentially more expressive than an\nequivalent formula in the worst case, since the circuit can reuse\nsubcircuits multiple times, whereas a formula cannot reuse subformulas\nmore than once. Thus creating a Boolean formula from a Boolean circuit\nin this way may be infeasible if the circuit is large.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"import matplotlib.pyplot as plt\nimport networkx as nx\n\n\ndef circuit_to_formula(circuit):\n # Convert the circuit to an equivalent formula.\n formula = nx.dag_to_branching(circuit)\n # Transfer the operator or variable labels for each node from the\n # circuit to the formula.\n for v in formula:\n source = formula.nodes[v][\"source\"]\n formula.nodes[v][\"label\"] = circuit.nodes[source][\"label\"]\n return formula\n\n\ndef formula_to_string(formula):\n def _to_string(formula, root):\n # If there are no children, this is a variable node.\n label = formula.nodes[root][\"label\"]\n if not formula[root]:\n return label\n # Otherwise, this is an operator.\n children = formula[root]\n # If one child, the label must be a NOT operator.\n if len(children) == 1:\n child = nx.utils.arbitrary_element(children)\n return f\"{label}({_to_string(formula, child)})\"\n # NB \"left\" and \"right\" here are a little misleading: there is\n # no order on the children of a node. That's okay because the\n # Boolean AND and OR operators are symmetric. It just means that\n # the order of the operands cannot be predicted and hence the\n # function does not necessarily behave the same way on every\n # invocation.\n left, right = formula[root]\n left_subformula = _to_string(formula, left)\n right_subformula = _to_string(formula, right)\n return f\"({left_subformula} {label} {right_subformula})\"\n\n root = next(v for v, d in formula.in_degree() if d == 0)\n return _to_string(formula, root)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Create an example Boolean circuit.\n\nThis circuit has a \u2227 at the output and two \u2228s at the next layer.\nThe third layer has a variable x that appears in the left \u2228, a\nvariable y that appears in both the left and right \u2228s, and a\nnegation for the variable z that appears as the sole node in the\nfourth layer.\n\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"circuit = nx.DiGraph()\n# Layer 0\ncircuit.add_node(0, label=\"\u2227\", layer=0)\n# Layer 1\ncircuit.add_node(1, label=\"\u2228\", layer=1)\ncircuit.add_node(2, label=\"\u2228\", layer=1)\ncircuit.add_edge(0, 1)\ncircuit.add_edge(0, 2)\n# Layer 2\ncircuit.add_node(3, label=\"x\", layer=2)\ncircuit.add_node(4, label=\"y\", layer=2)\ncircuit.add_node(5, label=\"\u00ac\", layer=2)\ncircuit.add_edge(1, 3)\ncircuit.add_edge(1, 4)\ncircuit.add_edge(2, 4)\ncircuit.add_edge(2, 5)\n# Layer 3\ncircuit.add_node(6, label=\"z\", layer=3)\ncircuit.add_edge(5, 6)\n# Convert the circuit to an equivalent formula.\nformula = circuit_to_formula(circuit)\nprint(formula_to_string(formula))\n\n\nlabels = nx.get_node_attributes(circuit, \"label\")\noptions = {\n \"node_size\": 600,\n \"alpha\": 0.5,\n \"node_color\": \"blue\",\n \"labels\": labels,\n \"font_size\": 22,\n}\nplt.figure(figsize=(8, 8))\npos = nx.multipartite_layout(circuit, subset_key=\"layer\")\nnx.draw_networkx(circuit, pos, **options)\nplt.title(formula_to_string(formula))\nplt.axis(\"equal\")\nplt.show()"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.7"
}
},
"nbformat": 4,
"nbformat_minor": 0
}
Generated by dwww version 1.16 on Wed Apr 8 10:56:16 CEST 2026.