Truth assignments and clause simplification To solve a SAT instance, we need to search for a truth assignment to its propositional variables that will make all the clauses true. We will search for such a truth assignment by trying to build it one variable at a time. So a basic operation on a clause will be:
Given a clause, and a truth assignment for one variable, compute the result on the clause.
What is the result on the clause? Consider a clause with representation c (thus, c is a set of integers) and a truth assignment (recall that can be positive or negative, depending on whether it assigns True or False to p). There are three cases:
If ∈c, then the literal of c is true, and so is the whole clause. We return True to signify it.
If −∈c, then the − literal of c is false, and it cannot help make the clause true. We return the clause c∖{−}, which corresponds to the remaining ways of making the clause true under assignment .
If neither nor − is in c, then we return c itself, as c is not affected by the truth assignment .
Based on the above discussion, implement a simplify method for a Clause that, given a truth assignment, returns a simplified clause or True.
# Exercise: define simplify def clause_simplify(self, i): """Computes the result simplify the clause according to the truth assignment i.""" # YOUR CODE HERE