HW2 Code Generation for Propositional Logic
This homework is based on the homework 1.
Given a Boolan formula F, the Boolean satisfiability problem asks if there are values for the
variables in F that makes the F to be True. For example, in G= P/\(Q\/!P), G evaluates to True
for P=True and Q=True. We call G satisfiable and (P=True, Q=True) a satisfying assignment for
G.
In this homework, you are asked to use the parser in HW1 and pysmt
(https://github.com/pysmt/pysmt) to (1) generate python code that represent the constraints
represented by propositions to an equivalents logical formula using pysmt APIs, (2) run the
python code in the previous step to check the satisfiability of the formula.
Your program will take a file containing a set of propositions and prints the result of the
satisfiability of conjunction of the propositions.
Example 1:
Input:
P /\ !Q
Corresponding python code:
from pysmt.shortcuts import Symbol, And, Not, is_sat
P = Symbol("P") # Default type is Boolean
Q = Symbol("Q")
f = And(P, Not(Q))
print is_sat(f)
$ python main.py constraints.txt
True
Example 2:
Input:
P /\ !Q, !P<=>!Q
python code:
from pysmt.shortcuts import Symbol, And, Iff, Not, is_sat
P = Symbol("P") # Default type is Boolean
Q = Symbol("Q")
prop1 = And(P, Not(varB))
prop2 = Iff(Not(P),Not(Q))
f = And(prop1, prop2)
print is_sat(f)
$ python main.py constraints.txt
True
