Newer
Older
3001
3002
3003
3004
3005
3006
3007
3008
3009
3010
3011
3012
3013
3014
3015
3016
3017
3018
3019
3020
3021
3022
3023
3024
3025
3026
3027
3028
3029
3030
3031
3032
3033
3034
3035
3036
3037
3038
3039
3040
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050
3051
3052
3053
3054
3055
3056
3057
3058
3059
3060
3061
3062
3063
3064
3065
3066
3067
3068
3069
3070
3071
3072
3073
3074
3075
3076
3077
3078
3079
3080
3081
3082
3083
3084
3085
3086
3087
3088
3089
3090
3091
3092
3093
3094
3095
3096
3097
3098
"body .nv { color: #19177C } /* Name.Variable */\n",
"body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
"body .w { color: #bbbbbb } /* Text.Whitespace */\n",
"body .mb { color: #666666 } /* Literal.Number.Bin */\n",
"body .mf { color: #666666 } /* Literal.Number.Float */\n",
"body .mh { color: #666666 } /* Literal.Number.Hex */\n",
"body .mi { color: #666666 } /* Literal.Number.Integer */\n",
"body .mo { color: #666666 } /* Literal.Number.Oct */\n",
"body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
"body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
"body .sc { color: #BA2121 } /* Literal.String.Char */\n",
"body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
"body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
"body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
"body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
"body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
"body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
"body .sx { color: #008000 } /* Literal.String.Other */\n",
"body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
"body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
"body .ss { color: #19177C } /* Literal.String.Symbol */\n",
"body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
"body .fm { color: #0000FF } /* Name.Function.Magic */\n",
"body .vc { color: #19177C } /* Name.Variable.Class */\n",
"body .vg { color: #19177C } /* Name.Variable.Global */\n",
"body .vi { color: #19177C } /* Name.Variable.Instance */\n",
"body .vm { color: #19177C } /* Name.Variable.Magic */\n",
"body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
"\n",
" </style>\n",
"</head>\n",
"<body>\n",
"<h2></h2>\n",
"\n",
"<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">WalkSAT</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">p</span><span class=\"o\">=</span><span class=\"mf\">0.5</span><span class=\"p\">,</span> <span class=\"n\">max_flips</span><span class=\"o\">=</span><span class=\"mi\">10000</span><span class=\"p\">):</span>\n",
" <span class=\"sd\">"""Checks for satisfiability of all clauses by randomly flipping values of variables</span>\n",
"<span class=\"sd\"> """</span>\n",
" <span class=\"c1\"># Set of all symbols in all clauses</span>\n",
" <span class=\"n\">symbols</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">sym</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span> <span class=\"k\">for</span> <span class=\"n\">sym</span> <span class=\"ow\">in</span> <span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)}</span>\n",
" <span class=\"c1\"># model is a random assignment of true/false to the symbols in clauses</span>\n",
" <span class=\"n\">model</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">s</span><span class=\"p\">:</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">([</span><span class=\"bp\">True</span><span class=\"p\">,</span> <span class=\"bp\">False</span><span class=\"p\">])</span> <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">symbols</span><span class=\"p\">}</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">i</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">max_flips</span><span class=\"p\">):</span>\n",
" <span class=\"n\">satisfied</span><span class=\"p\">,</span> <span class=\"n\">unsatisfied</span> <span class=\"o\">=</span> <span class=\"p\">[],</span> <span class=\"p\">[]</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
" <span class=\"p\">(</span><span class=\"n\">satisfied</span> <span class=\"k\">if</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)</span> <span class=\"k\">else</span> <span class=\"n\">unsatisfied</span><span class=\"p\">)</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)</span>\n",
" <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">unsatisfied</span><span class=\"p\">:</span> <span class=\"c1\"># if model satisfies all the clauses</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">model</span>\n",
" <span class=\"n\">clause</span> <span class=\"o\">=</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">(</span><span class=\"n\">unsatisfied</span><span class=\"p\">)</span>\n",
" <span class=\"k\">if</span> <span class=\"n\">probability</span><span class=\"p\">(</span><span class=\"n\">p</span><span class=\"p\">):</span>\n",
" <span class=\"n\">sym</span> <span class=\"o\">=</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">(</span><span class=\"nb\">list</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)))</span>\n",
" <span class=\"k\">else</span><span class=\"p\">:</span>\n",
" <span class=\"c1\"># Flip the symbol in clause that maximizes number of sat. clauses</span>\n",
" <span class=\"k\">def</span> <span class=\"nf\">sat_count</span><span class=\"p\">(</span><span class=\"n\">sym</span><span class=\"p\">):</span>\n",
" <span class=\"c1\"># Return the the number of clauses satisfied after flipping the symbol.</span>\n",
" <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
" <span class=\"n\">count</span> <span class=\"o\">=</span> <span class=\"nb\">len</span><span class=\"p\">([</span><span class=\"n\">clause</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span> <span class=\"k\">if</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)])</span>\n",
" <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">count</span>\n",
" <span class=\"n\">sym</span> <span class=\"o\">=</span> <span class=\"n\">argmax</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">),</span> <span class=\"n\">key</span><span class=\"o\">=</span><span class=\"n\">sat_count</span><span class=\"p\">)</span>\n",
" <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
" <span class=\"c1\"># If no solution is found within the flip limit, we return failure</span>\n",
" <span class=\"k\">return</span> <span class=\"bp\">None</span>\n",
"</pre></div>\n",
"</body>\n",
"</html>\n"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"psource(WalkSAT)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The function takes three arguments:\n",
"<br>\n",
"1. The `clauses` we want to satisfy.\n",
"<br>\n",
"2. The probability `p` of randomly changing a symbol.\n",
"<br>\n",
"3. The maximum number of flips (`max_flips`) the algorithm will run for. If the clauses are still unsatisfied, the algorithm returns `None` to denote failure.\n",
"<br>\n",
"The algorithm is identical in concept to Hill climbing and the code isn't difficult to understand.\n",
"<br>\n",
"<br>\n",
"Let's see a few examples of usage."
]
},
{
"cell_type": "code",
"outputs": [],
"source": [
"A, B, C, D = expr('A, B, C, D')"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{A: True, B: True, C: False, D: True}"
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"WalkSAT([A, B, ~C, D], 0.5, 100)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This is a simple case to show that the algorithm converges."
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"WalkSAT([A & B, A & C], 0.5, 100)"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{A: True, B: True, C: True, D: True}"
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"WalkSAT([A & B, C & D, C & B], 0.5, 100)"
]
},
{
"cell_type": "code",
3176
3177
3178
3179
3180
3181
3182
3183
3184
3185
3186
3187
3188
3189
3190
3191
3192
3193
3194
3195
3196
3197
3198
3199
"metadata": {},
"outputs": [],
"source": [
"WalkSAT([A & B, C | D, ~(D | B)], 0.5, 1000)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This one doesn't give any output because WalkSAT did not find any model where these clauses hold. We can solve these clauses to see that they together form a contradiction and hence, it isn't supposed to have a solution."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"One point of difference between this algorithm and the `dpll_satisfiable` algorithms is that both these algorithms take inputs differently. \n",
"For WalkSAT to take complete sentences as input, \n",
"we can write a helper function that converts the input sentence into conjunctive normal form and then calls WalkSAT with the list of conjuncts of the CNF form of the sentence."
]
},
{
"cell_type": "code",
"outputs": [],
"source": [
"def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n",
" return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we can call `WalkSAT_CNF` and `DPLL_Satisfiable` with the same arguments."
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
3227
3228
3229
3230
3231
3232
3233
3234
3235
3236
3237
3238
3239
3240
3241
3242
3243
3244
3245
3246
3247
3248
3249
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"WalkSAT_CNF((A & B) | (C & ~A) | (B & ~D), 0.5, 1000)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It works!\n",
"<br>\n",
"Notice that the solution generated by WalkSAT doesn't omit variables that the sentence doesn't depend upon. \n",
"If the sentence is independent of a particular variable, the solution contains a random value for that variable because of the stochastic nature of the algorithm.\n",
"<br>\n",
"<br>\n",
"Let's compare the runtime of WalkSAT and DPLL for a few cases. We will use the `%%timeit` magic to do this."
]
},
{
"cell_type": "code",
"outputs": [],
"source": [
"sentence_1 = A |'<=>'| B\n",
"sentence_2 = (A & B) | (C & ~A) | (B & ~D)\n",
"sentence_3 = (A | (B & C)) |'<=>'| ((A | B) & (A | C))"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1.55 ms ± 64.6 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n"
]
}
],
"source": [
"%%timeit\n",
"dpll_satisfiable(sentence_1)\n",
"dpll_satisfiable(sentence_2)\n",
"dpll_satisfiable(sentence_3)"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"1.02 ms ± 6.92 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n"
]
}
],
"source": [
"%%timeit\n",
"WalkSAT_CNF(sentence_1)\n",
"WalkSAT_CNF(sentence_2)\n",
"WalkSAT_CNF(sentence_3)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On an average, for solvable cases, `WalkSAT` is quite faster than `dpll` because, for a small number of variables, \n",
"`WalkSAT` can reduce the search space significantly. \n",
"Results can be different for sentences with more symbols though.\n",
"Feel free to play around with this to understand the trade-offs of these algorithms better."
]
},
3309
3310
3311
3312
3313
3314
3315
3316
3317
3318
3319
3320
3321
3322
3323
3324
3325
3326
3327
3328
3329
3330
3331
3332
3333
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### SATPlan"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this section we show how to make plans by logical inference. The basic idea is very simple. It includes the following three steps:\n",
"1. Constuct a sentence that includes:\n",
" 1. A colection of assertions about the initial state.\n",
" 2. The successor-state axioms for all the possible actions at each time up to some maximum time t.\n",
" 3. The assertion that the goal is achieved at time t.\n",
"2. Present the whole sentence to a SAT solver.\n",
"3. Assuming a model is found, extract from the model those variables that represent actions and are assigned true. Together they represent a plan to achieve the goals.\n",
"\n",
"\n",
"Lets have a look at the algorithm"
]
},
{
"cell_type": "code",
3335
3336
3337
3338
3339
3340
3341
3342
3343
3344
3345
3346
3347
3348
3349
3350
3351
3352
3353
3354
3355
3356
3357
3358
3359
3360
3361
3362
3363
3364
3365
3366
3367
3368
3369
3370
3371
3372
3373
3374
3375
3376
3377
3378
3379
3380
3381
3382
3383
3384
3385
3386
3387
3388
3389
3390
3391
3392
3393
3394
3395
3396
3397
3398
3399
3400
3401
3402
3403
3404
3405
3406
3407
3408
3409
3410
3411
3412
3413
3414
3415
3416
3417
3418
3419
3420
3421
3422
3423
3424
3425
3426
3427
3428
3429
3430
3431
3432
3433
3434
3435
3436
3437
3438
3439
3440
3441
3442
3443
3444
3445
3446
3447
3448
3449
3450
3451
3452
3453
3454
3455
3456
3457
3458
3459
3460
3461
3462
3463
3464
3465
3466
3467
3468
3469
3470
3471
3472
3473
3474
3475
3476
3477
3478
3479
3480
3481
3482
3483
3484
3485
3486
3487
3488
3489
3490
3491
3492
3493
3494
3495
3496
3497
3498
3499
3500
3501
3502
3503
3504
3505
3506
3507
3508
3509
3510
3511
3512
3513
3514
3515
3516
3517
3518
3519
3520
3521
3522
3523
3524
3525
3526
3527
3528
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
" \"http://www.w3.org/TR/html4/strict.dtd\">\n",
"\n",
"<html>\n",
"<head>\n",
" <title></title>\n",
" <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
" <style type=\"text/css\">\n",
"td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
"span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
"pre { line-height: 125%; }\n",
"body .hll { background-color: #ffffcc }\n",
"body { background: #f8f8f8; }\n",
"body .c { color: #408080; font-style: italic } /* Comment */\n",
"body .err { border: 1px solid #FF0000 } /* Error */\n",
"body .k { color: #008000; font-weight: bold } /* Keyword */\n",
"body .o { color: #666666 } /* Operator */\n",
"body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
"body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
"body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
"body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
"body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
"body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
"body .gd { color: #A00000 } /* Generic.Deleted */\n",
"body .ge { font-style: italic } /* Generic.Emph */\n",
"body .gr { color: #FF0000 } /* Generic.Error */\n",
"body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
"body .gi { color: #00A000 } /* Generic.Inserted */\n",
"body .go { color: #888888 } /* Generic.Output */\n",
"body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
"body .gs { font-weight: bold } /* Generic.Strong */\n",
"body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
"body .gt { color: #0044DD } /* Generic.Traceback */\n",
"body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
"body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
"body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
"body .kp { color: #008000 } /* Keyword.Pseudo */\n",
"body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
"body .kt { color: #B00040 } /* Keyword.Type */\n",
"body .m { color: #666666 } /* Literal.Number */\n",
"body .s { color: #BA2121 } /* Literal.String */\n",
"body .na { color: #7D9029 } /* Name.Attribute */\n",
"body .nb { color: #008000 } /* Name.Builtin */\n",
"body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
"body .no { color: #880000 } /* Name.Constant */\n",
"body .nd { color: #AA22FF } /* Name.Decorator */\n",
"body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
"body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
"body .nf { color: #0000FF } /* Name.Function */\n",
"body .nl { color: #A0A000 } /* Name.Label */\n",
"body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
"body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
"body .nv { color: #19177C } /* Name.Variable */\n",
"body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
"body .w { color: #bbbbbb } /* Text.Whitespace */\n",
"body .mb { color: #666666 } /* Literal.Number.Bin */\n",
"body .mf { color: #666666 } /* Literal.Number.Float */\n",
"body .mh { color: #666666 } /* Literal.Number.Hex */\n",
"body .mi { color: #666666 } /* Literal.Number.Integer */\n",
"body .mo { color: #666666 } /* Literal.Number.Oct */\n",
"body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
"body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
"body .sc { color: #BA2121 } /* Literal.String.Char */\n",
"body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
"body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
"body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
"body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
"body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
"body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
"body .sx { color: #008000 } /* Literal.String.Other */\n",
"body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
"body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
"body .ss { color: #19177C } /* Literal.String.Symbol */\n",
"body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
"body .fm { color: #0000FF } /* Name.Function.Magic */\n",
"body .vc { color: #19177C } /* Name.Variable.Class */\n",
"body .vg { color: #19177C } /* Name.Variable.Global */\n",
"body .vi { color: #19177C } /* Name.Variable.Instance */\n",
"body .vm { color: #19177C } /* Name.Variable.Magic */\n",
"body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
"\n",
" </style>\n",
"</head>\n",
"<body>\n",
"<h2></h2>\n",
"\n",
"<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">SAT_plan</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">t_max</span><span class=\"p\">,</span> <span class=\"n\">SAT_solver</span><span class=\"o\">=</span><span class=\"n\">dpll_satisfiable</span><span class=\"p\">):</span>\n",
" <span class=\"sd\">"""Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.</span>\n",
"<span class=\"sd\"> [Figure 7.22]"""</span>\n",
"\n",
" <span class=\"c1\"># Functions used by SAT_plan</span>\n",
" <span class=\"k\">def</span> <span class=\"nf\">translate_to_SAT</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">time</span><span class=\"p\">):</span>\n",
" <span class=\"n\">clauses</span> <span class=\"o\">=</span> <span class=\"p\">[]</span>\n",
" <span class=\"n\">states</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">state</span> <span class=\"k\">for</span> <span class=\"n\">state</span> <span class=\"ow\">in</span> <span class=\"n\">transition</span><span class=\"p\">]</span>\n",
"\n",
" <span class=\"c1\"># Symbol claiming state s at time t</span>\n",
" <span class=\"n\">state_counter</span> <span class=\"o\">=</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">count</span><span class=\"p\">()</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"o\">+</span><span class=\"mi\">1</span><span class=\"p\">):</span>\n",
" <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"n\">Expr</span><span class=\"p\">(</span><span class=\"s2\">"State_{}"</span><span class=\"o\">.</span><span class=\"n\">format</span><span class=\"p\">(</span><span class=\"nb\">next</span><span class=\"p\">(</span><span class=\"n\">state_counter</span><span class=\"p\">)))</span>\n",
"\n",
" <span class=\"c1\"># Add initial state axiom</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"mi\">0</span><span class=\"p\">])</span>\n",
"\n",
" <span class=\"c1\"># Add goal state axiom</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">time</span><span class=\"p\">])</span>\n",
"\n",
" <span class=\"c1\"># All possible transitions</span>\n",
" <span class=\"n\">transition_counter</span> <span class=\"o\">=</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">count</span><span class=\"p\">()</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">action</span> <span class=\"ow\">in</span> <span class=\"n\">transition</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">]:</span>\n",
" <span class=\"n\">s_</span> <span class=\"o\">=</span> <span class=\"n\">transition</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">][</span><span class=\"n\">action</span><span class=\"p\">]</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"p\">):</span>\n",
" <span class=\"c1\"># Action 'action' taken from state 's' at time 't' to reach 's_'</span>\n",
" <span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"n\">Expr</span><span class=\"p\">(</span>\n",
" <span class=\"s2\">"Transition_{}"</span><span class=\"o\">.</span><span class=\"n\">format</span><span class=\"p\">(</span><span class=\"nb\">next</span><span class=\"p\">(</span><span class=\"n\">transition_counter</span><span class=\"p\">)))</span>\n",
"\n",
" <span class=\"c1\"># Change the state from s to s_</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">|</span><span class=\"s1\">'==>'</span><span class=\"o\">|</span> <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">])</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">|</span><span class=\"s1\">'==>'</span><span class=\"o\">|</span> <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s_</span><span class=\"p\">,</span> <span class=\"n\">t</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">])</span>\n",
"\n",
" <span class=\"c1\"># Allow only one state at any time</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"o\">+</span><span class=\"mi\">1</span><span class=\"p\">):</span>\n",
" <span class=\"c1\"># must be a state at any time</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">'|'</span><span class=\"p\">,</span> <span class=\"p\">[</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">]))</span>\n",
"\n",
" <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">s_</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">[</span><span class=\"n\">states</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">:]:</span>\n",
" <span class=\"c1\"># for each pair of states s, s_ only one is possible at time t</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">((</span><span class=\"o\">~</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">])</span> <span class=\"o\">|</span> <span class=\"p\">(</span><span class=\"o\">~</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s_</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]))</span>\n",
"\n",
" <span class=\"c1\"># Restrict to one transition per timestep</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"p\">):</span>\n",
" <span class=\"c1\"># list of possible transitions at time t</span>\n",
" <span class=\"n\">transitions_t</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">tr</span> <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">action_sym</span> <span class=\"k\">if</span> <span class=\"n\">tr</span><span class=\"p\">[</span><span class=\"mi\">2</span><span class=\"p\">]</span> <span class=\"o\">==</span> <span class=\"n\">t</span><span class=\"p\">]</span>\n",
"\n",
" <span class=\"c1\"># make sure at least one of the transitions happens</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">'|'</span><span class=\"p\">,</span> <span class=\"p\">[</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr</span><span class=\"p\">]</span> <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">]))</span>\n",
"\n",
" <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">:</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">tr_</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">[</span><span class=\"n\">transitions_t</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">tr</span><span class=\"p\">)</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">:]:</span>\n",
" <span class=\"c1\"># there cannot be two transitions tr and tr_ at time t</span>\n",
" <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"o\">~</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr</span><span class=\"p\">]</span> <span class=\"o\">|</span> <span class=\"o\">~</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr_</span><span class=\"p\">])</span>\n",
"\n",
" <span class=\"c1\"># Combine the clauses to form the cnf</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">'&'</span><span class=\"p\">,</span> <span class=\"n\">clauses</span><span class=\"p\">)</span>\n",
"\n",
" <span class=\"k\">def</span> <span class=\"nf\">extract_solution</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">):</span>\n",
" <span class=\"n\">true_transitions</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">t</span> <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"n\">action_sym</span> <span class=\"k\">if</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">t</span><span class=\"p\">]]]</span>\n",
" <span class=\"c1\"># Sort transitions based on time, which is the 3rd element of the tuple</span>\n",
" <span class=\"n\">true_transitions</span><span class=\"o\">.</span><span class=\"n\">sort</span><span class=\"p\">(</span><span class=\"n\">key</span><span class=\"o\">=</span><span class=\"k\">lambda</span> <span class=\"n\">x</span><span class=\"p\">:</span> <span class=\"n\">x</span><span class=\"p\">[</span><span class=\"mi\">2</span><span class=\"p\">])</span>\n",
" <span class=\"k\">return</span> <span class=\"p\">[</span><span class=\"n\">action</span> <span class=\"k\">for</span> <span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">time</span> <span class=\"ow\">in</span> <span class=\"n\">true_transitions</span><span class=\"p\">]</span>\n",
"\n",
" <span class=\"c1\"># Body of SAT_plan algorithm</span>\n",
" <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">t_max</span><span class=\"p\">):</span>\n",
" <span class=\"c1\"># dictionaries to help extract the solution from model</span>\n",
" <span class=\"n\">state_sym</span> <span class=\"o\">=</span> <span class=\"p\">{}</span>\n",
" <span class=\"n\">action_sym</span> <span class=\"o\">=</span> <span class=\"p\">{}</span>\n",
"\n",
" <span class=\"n\">cnf</span> <span class=\"o\">=</span> <span class=\"n\">translate_to_SAT</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">)</span>\n",
" <span class=\"n\">model</span> <span class=\"o\">=</span> <span class=\"n\">SAT_solver</span><span class=\"p\">(</span><span class=\"n\">cnf</span><span class=\"p\">)</span>\n",
" <span class=\"k\">if</span> <span class=\"n\">model</span> <span class=\"ow\">is</span> <span class=\"ow\">not</span> <span class=\"bp\">False</span><span class=\"p\">:</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">extract_solution</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">)</span>\n",
" <span class=\"k\">return</span> <span class=\"bp\">None</span>\n",
"</pre></div>\n",
"</body>\n",
"</html>\n"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"psource(SAT_plan)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's see few examples of its usage. First we define a transition and then call `SAT_plan`."
]
},
{
"cell_type": "code",
3530
3531
3532
3533
3534
3535
3536
3537
3538
3539
3540
3541
3542
3543
3544
3545
3546
3547
3548
3549
3550
3551
3552
3553
3554
3555
3556
3557
3558
3559
3560
3561
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"None\n",
"['Right']\n",
"['Left', 'Left']\n"
]
}
],
"source": [
"transition = {'A': {'Left': 'A', 'Right': 'B'},\n",
" 'B': {'Left': 'A', 'Right': 'C'},\n",
" 'C': {'Left': 'B', 'Right': 'C'}}\n",
"\n",
"\n",
"print(SAT_plan('A', transition, 'C', 2)) \n",
"print(SAT_plan('A', transition, 'B', 3))\n",
"print(SAT_plan('C', transition, 'A', 3))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let us do the same for another transition."
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"['Right', 'Down']\n"
]
}
],
"source": [
"transition = {(0, 0): {'Right': (0, 1), 'Down': (1, 0)},\n",
" (0, 1): {'Left': (1, 0), 'Down': (1, 1)},\n",
" (1, 0): {'Right': (1, 0), 'Up': (1, 0), 'Left': (1, 0), 'Down': (1, 0)},\n",
" (1, 1): {'Left': (1, 0), 'Up': (0, 1)}}\n",
"\n",
"\n",
"print(SAT_plan((0, 0), transition, (1, 1), 4))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## First-Order Logic Knowledge Bases: `FolKB`\n",
"\n",
"The class `FolKB` can be used to represent a knowledge base of First-order logic sentences. You would initialize and use it the same way as you would for `PropKB` except that the clauses are first-order definite clauses. We will see how to write such clauses to create a database and query them in the following sections."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Criminal KB\n",
"In this section we create a `FolKB` based on the following paragraph.<br/>\n",
"<em>The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.</em><br/>\n",
"The first step is to extract the facts and convert them into first-order definite clauses. Extracting the facts from data alone is a challenging task. Fortunately, we have a small paragraph and can do extraction and conversion manually. We'll store the clauses in list aptly named `clauses`."
]
},
{
"cell_type": "code",
"execution_count": 69,
"metadata": {},
"outputs": [],
"source": [
"clauses = []"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<em>“... it is a crime for an American to sell weapons to hostile nations”</em><br/>\n",
"The keywords to look for here are 'crime', 'American', 'sell', 'weapon' and 'hostile'. We use predicate symbols to make meaning of them.\n",
"\n",
"* `Criminal(x)`: `x` is a criminal\n",
"* `American(x)`: `x` is an American\n",
"* `Sells(x ,y, z)`: `x` sells `y` to `z`\n",
"* `Weapon(x)`: `x` is a weapon\n",
"* `Hostile(x)`: `x` is a hostile nation\n",
"\n",
"Let us now combine them with appropriate variable naming to depict the meaning of the sentence. The criminal `x` is also the American `x` who sells weapon `y` to `z`, which is a hostile nation.\n",
"\n",
"$\\text{American}(x) \\land \\text{Weapon}(y) \\land \\text{Sells}(x, y, z) \\land \\text{Hostile}(z) \\implies \\text{Criminal} (x)$"
]
},
{
"cell_type": "code",
"execution_count": 70,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<em>\"The country Nono, an enemy of America\"</em><br/>\n",
"We now know that Nono is an enemy of America. We represent these nations using the constant symbols `Nono` and `America`. the enemy relation is show using the predicate symbol `Enemy`.\n",
"\n",
"$\\text{Enemy}(\\text{Nono}, \\text{America})$"
]
},
{
"cell_type": "code",
"execution_count": 71,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"Enemy(Nono, America)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<em>\"Nono ... has some missiles\"</em><br/>\n",
"This states the existence of some missile which is owned by Nono. $\\exists x \\text{Owns}(\\text{Nono}, x) \\land \\text{Missile}(x)$. We invoke existential instantiation to introduce a new constant `M1` which is the missile owned by Nono.\n",
"\n",
"$\\text{Owns}(\\text{Nono}, \\text{M1}), \\text{Missile}(\\text{M1})$"
]
},
{
"cell_type": "code",
"execution_count": 72,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"Owns(Nono, M1)\"))\n",
"clauses.append(expr(\"Missile(M1)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {
"collapsed": true
},
"source": [
"<em>\"All of its missiles were sold to it by Colonel West\"</em><br/>\n",
"If Nono owns something and it classifies as a missile, then it was sold to Nono by West.\n",
"\n",
"$\\text{Missile}(x) \\land \\text{Owns}(\\text{Nono}, x) \\implies \\text{Sells}(\\text{West}, x, \\text{Nono})$"
]
},
{
"cell_type": "code",
"execution_count": 73,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<em>\"West, who is American\"</em><br/>\n",
"West is an American.\n",
"\n",
"$\\text{American}(\\text{West})$"
]
},
{
"cell_type": "code",
"execution_count": 74,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"American(West)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We also know, from our understanding of language, that missiles are weapons and that an enemy of America counts as “hostile”.\n",
"\n",
"$\\text{Missile}(x) \\implies \\text{Weapon}(x), \\text{Enemy}(x, \\text{America}) \\implies \\text{Hostile}(x)$"
]
},
{
"cell_type": "code",
"execution_count": 75,
"metadata": {},
"outputs": [],
"source": [
"clauses.append(expr(\"Missile(x) ==> Weapon(x)\"))\n",
"clauses.append(expr(\"Enemy(x, America) ==> Hostile(x)\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now that we have converted the information into first-order definite clauses we can create our first-order logic knowledge base."
]
},
{
"cell_type": "code",
"execution_count": 76,
"metadata": {},
3749
3750
3751
3752
3753
3754
3755
3756
3757
3758
3759
3760
3761
3762
3763
3764
3765
3766
3767
3768
3769
3770
3771
3772
3773
3774
3775
3776
3777
3778
3779
3780
3781
3782
3783
3784
3785
3786
3787
3788
3789
3790
3791
3792
3793
3794
3795
3796
3797
3798
3799
3800
3801
3802
3803
3804
3805
3806
3807
3808
3809
3810
3811
3812
3813
3814
3815
3816
3817
3818
3819
3820
3821
3822
3823
3824
3825
3826
3827
3828
3829
3830
3831
3832
3833
3834
3835
3836
3837
3838
3839
3840
3841
3842
3843
3844
3845
3846
3847
3848
3849
3850
3851
3852
3853
3854
3855
3856
3857
3858
3859
3860
3861
3862
3863
3864
3865
3866
3867
3868
3869
3870
3871
3872
3873
3874
3875
3876
3877
3878
3879
3880
3881
3882
3883
3884
3885
3886
3887
3888
3889
3890
3891
3892
3893
3894
3895
3896
3897
3898
3899
3900
3901
3902
3903
3904
3905
3906
3907
3908
3909
3910
"crime_kb = FolKB(clauses)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `subst` helper function substitutes variables with given values in first-order logic statements.\n",
"This will be useful in later algorithms.\n",
"It's implementation is quite simple and self-explanatory."
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
" \"http://www.w3.org/TR/html4/strict.dtd\">\n",
"\n",
"<html>\n",
"<head>\n",
" <title></title>\n",
" <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
" <style type=\"text/css\">\n",
"td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
"span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
"pre { line-height: 125%; }\n",
"body .hll { background-color: #ffffcc }\n",
"body { background: #f8f8f8; }\n",
"body .c { color: #408080; font-style: italic } /* Comment */\n",
"body .err { border: 1px solid #FF0000 } /* Error */\n",
"body .k { color: #008000; font-weight: bold } /* Keyword */\n",
"body .o { color: #666666 } /* Operator */\n",
"body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
"body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
"body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
"body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
"body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
"body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
"body .gd { color: #A00000 } /* Generic.Deleted */\n",
"body .ge { font-style: italic } /* Generic.Emph */\n",
"body .gr { color: #FF0000 } /* Generic.Error */\n",
"body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
"body .gi { color: #00A000 } /* Generic.Inserted */\n",
"body .go { color: #888888 } /* Generic.Output */\n",
"body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
"body .gs { font-weight: bold } /* Generic.Strong */\n",
"body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
"body .gt { color: #0044DD } /* Generic.Traceback */\n",
"body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
"body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
"body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
"body .kp { color: #008000 } /* Keyword.Pseudo */\n",
"body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
"body .kt { color: #B00040 } /* Keyword.Type */\n",
"body .m { color: #666666 } /* Literal.Number */\n",
"body .s { color: #BA2121 } /* Literal.String */\n",
"body .na { color: #7D9029 } /* Name.Attribute */\n",
"body .nb { color: #008000 } /* Name.Builtin */\n",
"body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
"body .no { color: #880000 } /* Name.Constant */\n",
"body .nd { color: #AA22FF } /* Name.Decorator */\n",
"body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
"body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
"body .nf { color: #0000FF } /* Name.Function */\n",
"body .nl { color: #A0A000 } /* Name.Label */\n",
"body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
"body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
"body .nv { color: #19177C } /* Name.Variable */\n",
"body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
"body .w { color: #bbbbbb } /* Text.Whitespace */\n",
"body .mb { color: #666666 } /* Literal.Number.Bin */\n",
"body .mf { color: #666666 } /* Literal.Number.Float */\n",
"body .mh { color: #666666 } /* Literal.Number.Hex */\n",
"body .mi { color: #666666 } /* Literal.Number.Integer */\n",
"body .mo { color: #666666 } /* Literal.Number.Oct */\n",
"body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
"body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
"body .sc { color: #BA2121 } /* Literal.String.Char */\n",
"body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
"body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
"body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
"body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
"body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
"body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
"body .sx { color: #008000 } /* Literal.String.Other */\n",
"body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
"body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
"body .ss { color: #19177C } /* Literal.String.Symbol */\n",
"body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
"body .fm { color: #0000FF } /* Name.Function.Magic */\n",
"body .vc { color: #19177C } /* Name.Variable.Class */\n",
"body .vg { color: #19177C } /* Name.Variable.Global */\n",
"body .vi { color: #19177C } /* Name.Variable.Instance */\n",
"body .vm { color: #19177C } /* Name.Variable.Magic */\n",
"body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
"\n",
" </style>\n",
"</head>\n",
"<body>\n",
"<h2></h2>\n",
"\n",
"<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">subst</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">x</span><span class=\"p\">):</span>\n",
" <span class=\"sd\">"""Substitute the substitution s into the expression x.</span>\n",
"<span class=\"sd\"> >>> subst({x: 42, y:0}, F(x) + y)</span>\n",
"<span class=\"sd\"> (F(42) + 0)</span>\n",
"<span class=\"sd\"> """</span>\n",
" <span class=\"k\">if</span> <span class=\"nb\">isinstance</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"nb\">list</span><span class=\"p\">):</span>\n",
" <span class=\"k\">return</span> <span class=\"p\">[</span><span class=\"n\">subst</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">xi</span><span class=\"p\">)</span> <span class=\"k\">for</span> <span class=\"n\">xi</span> <span class=\"ow\">in</span> <span class=\"n\">x</span><span class=\"p\">]</span>\n",
" <span class=\"k\">elif</span> <span class=\"nb\">isinstance</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"nb\">tuple</span><span class=\"p\">):</span>\n",
" <span class=\"k\">return</span> <span class=\"nb\">tuple</span><span class=\"p\">([</span><span class=\"n\">subst</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">xi</span><span class=\"p\">)</span> <span class=\"k\">for</span> <span class=\"n\">xi</span> <span class=\"ow\">in</span> <span class=\"n\">x</span><span class=\"p\">])</span>\n",
" <span class=\"k\">elif</span> <span class=\"ow\">not</span> <span class=\"nb\">isinstance</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"n\">Expr</span><span class=\"p\">):</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">x</span>\n",
" <span class=\"k\">elif</span> <span class=\"n\">is_var_symbol</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"o\">.</span><span class=\"n\">op</span><span class=\"p\">):</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">s</span><span class=\"o\">.</span><span class=\"n\">get</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"n\">x</span><span class=\"p\">)</span>\n",
" <span class=\"k\">else</span><span class=\"p\">:</span>\n",
" <span class=\"k\">return</span> <span class=\"n\">Expr</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"o\">.</span><span class=\"n\">op</span><span class=\"p\">,</span> <span class=\"o\">*</span><span class=\"p\">[</span><span class=\"n\">subst</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">arg</span><span class=\"p\">)</span> <span class=\"k\">for</span> <span class=\"n\">arg</span> <span class=\"ow\">in</span> <span class=\"n\">x</span><span class=\"o\">.</span><span class=\"n\">args</span><span class=\"p\">])</span>\n",
"</pre></div>\n",
"</body>\n",
"</html>\n"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"psource(subst)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Here's an example of how `subst` can be used."
]
},
{
"cell_type": "code",
"execution_count": 78,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Owns(Nono, M1)"
]
},
"execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"subst({x: expr('Nono'), y: expr('M1')}, expr('Owns(x, y)'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Inference in First-Order Logic\n",
"In this section we look at a forward chaining and a backward chaining algorithm for `FolKB`. Both aforementioned algorithms rely on a process called <strong>unification</strong>, a key component of all first-order inference algorithms."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Unification\n",
"We sometimes require finding substitutions that make different logical expressions look identical. This process, called unification, is done by the `unify` algorithm. It takes as input two sentences and returns a <em>unifier</em> for them if one exists. A unifier is a dictionary which stores the substitutions required to make the two sentences identical. It does so by recursively unifying the components of a sentence, where the unification of a variable symbol `var` with a constant symbol `Const` is the mapping `{var: Const}`. Let's look at a few examples."
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{x: 3}"
]
},
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"unify(expr('x'), 3)"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{x: B}"
]
},
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"unify(expr('A(x)'), expr('A(B)'))"
]
},
{
"cell_type": "code",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{x: Bella, y: Dobby}"
]
},
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(y)'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In cases where there is no possible substitution that unifies the two sentences the function return `None`."
]
},
{
"cell_type": "code",