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
3099
3100
3101
3102
3103
3104
3105
3106
3107
3108
3109
3110
3111
3112
3113
3114
3115
3116
3117
"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\">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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
3200
3201
3202
3203
3204
3205
3206
3207
3208
3209
3210
3211
3212
3213
3214
3215
3216
3217
3218
3219
3220
3221
3222
"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",
"metadata": {
"collapsed": true
},
"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": [
3252
3253
3254
3255
3256
3257
3258
3259
3260
3261
3262
3263
3264
3265
3266
3267
3268
3269
3270
3271
3272
3273
3274
"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",
"metadata": {
"collapsed": true
},
"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."
]
},
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
{
"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",
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
3529
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
"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",
3557
3558
3559
3560
3561
3562
3563
3564
3565
3566
3567
3568
3569
3570
3571
3572
3573
3574
3575
3576
3577
3578
3579
3580
3581
3582
3583
3584
3585
3586
3587
3588
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
"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",
"metadata": {
"collapsed": true
},
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
3911
3912
3913
3914
3915
3916
3917
3918
3919
3920
3921
3922
3923
3924
3925
3926
3927
3928
3929
3930
3931
3932
3933
3934
3935
3936
3937
3938
3939
3940
3941
3942
3943
3944
3945
3946
3947
3948
3949
3950
3951
3952
3953
"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}"