CS 370 - February 17, 2025¶
homework 4 solutions
hw4¶
In [1]:
from utils4e import *
from logic import *
from notebook4e import psource
Problem 7.4
In [2]:
c = PropKB()
In [3]:
c.tell(expr('A & B'))
In [4]:
c.clauses
Out[4]:
[A, B]
In [5]:
c.ask_if_true(expr('A <=> B'))
Out[5]:
True
In [6]:
d=PropKB()
In [7]:
d.tell(expr('A <=> B'))
In [8]:
d.clauses
Out[8]:
[(A | ~B), (B | ~A)]
In [9]:
d.ask_if_true(expr('A | B'))
Out[9]:
False
In [10]:
e = PropKB()
In [11]:
e.tell(expr('A <=> B'))
In [12]:
e.clauses
Out[12]:
[(A | ~B), (B | ~A)]
In [13]:
e.ask_if_true(expr('~A | B'))
Out[13]:
True
In [14]:
f = PropKB()
In [15]:
f.tell(expr('(A | B) ==> C'))
In [16]:
f.clauses
Out[16]:
[(~A | C), (~B | C)]
In [17]:
f.ask_if_true(expr('(A ==> C) | (B ==> C)'))
Out[17]:
True
In [18]:
g = PropKB()
In [19]:
g.tell(expr('C | (~A & ~B)'))
In [20]:
g.clauses
Out[20]:
[(~A | C), (~B | C)]
In [21]:
g.ask_if_true(expr('(A ==> C) & (B ==> C)'))
Out[21]:
True
In [22]:
h = PropKB()
In [23]:
h.tell(expr('(A | B) & (~C | ~D | E)'))
In [24]:
h.clauses
Out[24]:
[(A | B), (~C | ~D | E)]
In [25]:
h.ask_if_true(expr('A | B'))
Out[25]:
True
In [26]:
i = PropKB()
In [27]:
i.tell(expr('(A | B) & (~C | ~D | E)'))
In [28]:
i.clauses
Out[28]:
[(A | B), (~C | ~D | E)]
In [29]:
i.ask_if_true(expr('(A | B) & (~D | E)'))
Out[29]:
False
7.4 (j)
In [30]:
A, B = expr('A, B')
In [32]:
dpll_satisfiable(A | B)
Out[32]:
{A: True}
In [33]:
dpll_satisfiable((A | B) & ~A)
Out[33]:
{B: True, A: False}
In [44]:
dpll_satisfiable(expr('A ==> B'))
Out[44]:
{A: False}
In [46]:
dpll_satisfiable(expr('(A | B) & ~ (A ==> B)'))
Out[46]:
{A: True, B: False}
7.4 (k)
In [52]:
expr('(A <=> B) & (~A | B)')
Out[52]:
((A <=> B) & (~A | B))
In [53]:
dpll_satisfiable(expr('(A <=> B) & (~A | B)'))
Out[53]:
{A: True, B: True}
7.4 (l)
In [54]:
expr('(A <=> B) <=> C')
Out[54]:
((A <=> B) <=> C)
In [55]:
dpll_satisfiable(expr('(A <=> B) <=> C'))
Out[55]:
{A: True, C: True, B: True}
In [66]:
to_cnf(expr('(A <=> B) <=> C'))
Out[66]:
((A | ~B | ~C) & (B | ~A | ~C) & (~B | ~A | C) & (A | ~A | C) & (~B | B | C) & (A | B | C))
In [69]:
WalkSAT([A], .5,100)
Out[69]:
{A: True}
Unicorn Problem 7.2¶
In [76]:
ukb = PropKB()
In [77]:
ukb.tell(expr('Mythical ==> Immortal'))
In [78]:
ukb.tell(expr('~Mythical ==> (~Immortal & Mammal)'))
In [79]:
ukb.tell(expr('(Immortal | Mammal) ==> Horned'))
In [80]:
ukb.tell(expr('Horned ==> Magical'))
In [81]:
ukb.clauses
Out[81]:
[(Immortal | ~Mythical), (~Immortal | Mythical), (Mammal | Mythical), (~Immortal | Horned), (~Mammal | Horned), (Magical | ~Horned)]
In [38]:
ukb.ask_if_true(expr('Mythical'))
Out[38]:
False
In [39]:
ukb.ask_if_true(expr('~Mythical'))
Out[39]:
False
In [40]:
ukb.ask_if_true(expr('Magical'))
Out[40]:
True
In [41]:
ukb.ask_if_true(expr('Horned'))
Out[41]:
True
In [82]:
ukb.ask_if_true(expr('Immortal'))
Out[82]:
False
In [83]:
ukb.ask_if_true(expr('Mammal'))
Out[83]:
False
In [84]:
ukb.ask_if_true(expr('Mythical'))
Out[84]:
False
7.7
In [85]:
A, B, C, D = expr('A, B, C, D')
7.7 (a)
In [87]:
dpll_satisfiable(expr('B | C'))
Out[87]:
{C: True}
7.7 (b)
In [88]:
expr('~ A | ~ B | ~ C | ~ D')
Out[88]:
(((~A | ~B) | ~C) | ~D)
In [89]:
dpll_satisfiable(expr('~ A | ~ B | ~ C | ~ D'))
Out[89]:
{A: False}
7.7 (c)
In [90]:
expr('(A <=> B) & A & ~B & C & D')
Out[90]:
(((((A <=> B) & A) & ~B) & C) & D)
In [91]:
dpll_satisfiable(expr('(A <=> B) & A & ~B & C & D'))
Out[91]:
False
In [ ]: