Let conjunctive normal form, consists in a conjunction of disjunctions of propositional variables and their complements, such asbe propositional variables. A SAT problem, represented in
The satisfiability question is: can we find a truth assignment to the variables that makes the expression true? In the above case, the answer is yes: we can take:
and any value for.
To represent an instance of SAT, we represent literals, clauses, and the overall expression, as follows.
Literals. We represent the literalvia the positive integer , and the literal via the negative integer .
Clauses. We represent a clause via the set of integers representing the clause literals.
For instance, we represent the clause via the set .
SAT problem. We represent a SAT problem (again, in conjunctive normal form) via the set consisting in the representation of its clauses. For instance, the problem
is represented by the set of sets:
There are various operations that we need to do on clauses, and on the overall SAT problem, to solve it. Thus, we encapsulate both clauses, and the SAT problem, in python classes, so we can associate the operations along with the representations.
We first define an auxiliary function, which tells us whether a set contains both an integer and its negative. This will be used, for instance, to detect whether a clause contains both a literal and its complement.
We are seeking a truth assignment for the propositional variables that makes the expression true, and so, that makes each clause true.
We represent the truth assignment that assigns True tovia the integer , and the truth assignment that assigns False to via . Thus, if you have a (positive or negative) literal , the truth assignment will make it true.
We represent truth assignments to multiple variables simply as the set of assignments to individual variables. For example, the truth assignment that assigns True toand False to will be represented via the set .
Question 1: Define 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(thus, 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 ). There are three cases:
- If , then the literal of is true, and so is the whole clause. We return True to signify it.
- If , then the literal of is false, and it cannot help make the clause true. We return the clause , which corresponds to the remaining ways of making the clause true under assignment .
- If neither nor is in , then we return itself, as 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 either a simplified clause, if some literals