diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb index cf804ae1788493c923a32f1813b4888873c8e9ee..f672d65ecb51b82a028ef0de456f2971073a1041 100644 --- a/notebooks/tutorials/prob_solver_intro.ipynb +++ b/notebooks/tutorials/prob_solver_intro.ipynb @@ -68,7 +68,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 3, "metadata": {}, "outputs": [ { @@ -77,7 +77,7 @@ "TRUE" ] }, - "execution_count": 1, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -96,16 +96,19 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (x = −10)" + "TRUE\n", + "\n", + "Solution:\n", + "\tx = −10" ] }, - "execution_count": 3, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -124,7 +127,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -133,7 +136,7 @@ "{−10,10}" ] }, - "execution_count": 4, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -152,16 +155,26 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (R = 8 ∧ S = 9 ∧ D = 7 ∧ E = 5 ∧ Y = 2 ∧ M = 1 ∧ N = 6 ∧ O = 0)" + "TRUE\n", + "\n", + "Solution:\n", + "\tR = 8\n", + "\tS = 9\n", + "\tD = 7\n", + "\tE = 5\n", + "\tY = 2\n", + "\tM = 1\n", + "\tN = 6\n", + "\tO = 0" ] }, - "execution_count": 5, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } @@ -184,16 +197,26 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (R = 0 ∧ S = 9 ∧ D = 0 ∧ E = 0 ∧ Y = 0 ∧ M = 1 ∧ N = 0 ∧ O = 0)" + "TRUE\n", + "\n", + "Solution:\n", + "\tR = 0\n", + "\tS = 9\n", + "\tD = 0\n", + "\tE = 0\n", + "\tY = 0\n", + "\tM = 1\n", + "\tN = 0\n", + "\tO = 0" ] }, - "execution_count": 6, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -215,7 +238,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -224,7 +247,7 @@ "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}" ] }, - "execution_count": 7, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -248,16 +271,25 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (P = 4 ∧ A = 1 ∧ S = 3 ∧ I = 0 ∧ K = 2 ∧ N = 9 ∧ O = 8)" + "TRUE\n", + "\n", + "Solution:\n", + "\tP = 4\n", + "\tA = 1\n", + "\tS = 3\n", + "\tI = 0\n", + "\tK = 2\n", + "\tN = 9\n", + "\tO = 8" ] }, - "execution_count": 10, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -280,16 +312,20 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)} ∧ n = 8)" + "TRUE\n", + "\n", + "Solution:\n", + "\tqueens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}\n", + "\tn = 8" ] }, - "execution_count": 8, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -304,16 +340,20 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (queens = {(1↦1),(2↦3),(3↦5),(4↦13),(5↦11),(6↦4),(7↦15),(8↦7),(9↦16),(10↦14),(11↦2),(12↦8),(13↦6),(14↦9),(15↦12),(16↦10)} ∧ n = 16)" + "TRUE\n", + "\n", + "Solution:\n", + "\tqueens = {(1↦1),(2↦3),(3↦5),(4↦13),(5↦11),(6↦4),(7↦15),(8↦7),(9↦16),(10↦14),(11↦2),(12↦8),(13↦6),(14↦9),(15↦12),(16↦10)}\n", + "\tn = 16" ] }, - "execution_count": 12, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -346,16 +386,21 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (A = TRUE ∧ B = TRUE ∧ C = FALSE)" + "TRUE\n", + "\n", + "Solution:\n", + "\tA = TRUE\n", + "\tB = TRUE\n", + "\tC = FALSE" ] }, - "execution_count": 14, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -375,7 +420,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -384,7 +429,7 @@ "{((TRUE↦TRUE)↦FALSE)}" ] }, - "execution_count": 15, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -404,16 +449,21 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (DOM = (1 ‥ 9) ∧ Board = {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(5↦3),(6↦2),(7↦9),(8↦4),(9↦5)}),(2↦{(1↦9),(2↦5),(3↦2),(4↦7),(5↦1),(6↦4),(7↦6),(8↦3),(9↦8)}),(3↦{(1↦4),(2↦3),(3↦6),(4↦8),(5↦9),(6↦5),(7↦7),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(5↦7),(6↦6),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(5↦8),(6↦1),(7↦2),(8↦9),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(4↦4),(5↦2),(6↦9),(7↦3),(8↦6),(9↦7)}),(7↦{(1↦1),(2↦9),(3↦4),(4↦2),(5↦6),(6↦7),(7↦5),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(4↦1),(5↦5),(6↦3),(7↦4),(8↦2),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(4↦9),(5↦4),(6↦8),(7↦1),(8↦7),(9↦6)})} ∧ SUBSQ = {{1,2,3},{4,5,6},{7,8,9}})" + "TRUE\n", + "\n", + "Solution:\n", + "\tDOM = (1 ‥ 9)\n", + "\tBoard = {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(5↦3),(6↦2),(7↦9),(8↦4),(9↦5)}),(2↦{(1↦9),(2↦5),(3↦2),(4↦7),(5↦1),(6↦4),(7↦6),(8↦3),(9↦8)}),(3↦{(1↦4),(2↦3),(3↦6),(4↦8),(5↦9),(6↦5),(7↦7),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(5↦7),(6↦6),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(5↦8),(6↦1),(7↦2),(8↦9),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(4↦4),(5↦2),(6↦9),(7↦3),(8↦6),(9↦7)}),(7↦{(1↦1),(2↦9),(3↦4),(4↦2),(5↦6),(6↦7),(7↦5),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(4↦1),(5↦5),(6↦3),(7↦4),(8↦2),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(4↦9),(5↦4),(6↦8),(7↦1),(8↦7),(9↦6)})}\n", + "\tSUBSQ = {{1,2,3},{4,5,6},{7,8,9}}" ] }, - "execution_count": 3, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -464,16 +514,20 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (stolen = {(16↦2),(17↦4),(23↦0),(24↦0),(39↦0),(40↦0)} ∧ coins = {16,17,23,24,39,40})" + "TRUE\n", + "\n", + "Solution:\n", + "\tstolen = {(16↦2),(17↦4),(23↦0),(24↦0),(39↦0),(40↦0)}\n", + "\tcoins = {16,17,23,24,39,40}" ] }, - "execution_count": 4, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -493,16 +547,23 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 16, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TRUE (Persons = {\"Agatha\",\"Charles\",\"butler\"} ∧ richer = {(\"Agatha\"↦\"Charles\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")} ∧ victim = \"Agatha\" ∧ killer = \"Agatha\" ∧ hates = {(\"Agatha\"↦\"Agatha\"),(\"Agatha\"↦\"Charles\"),(\"Charles\"↦\"butler\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")})" + "TRUE\n", + "\n", + "Solution:\n", + "\tPersons = {\"Agatha\",\"Charles\",\"butler\"}\n", + "\tricher = {(\"Agatha\"↦\"Charles\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")}\n", + "\tvictim = \"Agatha\"\n", + "\tkiller = \"Agatha\"\n", + "\thates = {(\"Agatha\"↦\"Agatha\"),(\"Agatha\"↦\"Charles\"),(\"Charles\"↦\"butler\"),(\"butler\"↦\"Agatha\"),(\"butler\"↦\"Charles\")}" ] }, - "execution_count": 5, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -527,6 +588,13 @@ " victim = \"Agatha\"" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null,