### Python海龟宝典含200多个原创的用turtle模块制作的创意程序，原名《Python趣味编程200例》。准备参加全国创意编程与智能设计大赛的同学们可以用来做参考。

Let 𝑝1,𝑝2,p1,p2,… be propositional variables. A SAT problem, represented in conjunctive normal form, consists in a conjunction of disjunctions of propositional variables and their complements, such as

(𝑝1𝑝¯2𝑝3)(𝑝2𝑝5).(p1∨p¯2∨p3)∧(p2∨p5).

We call each conjuct a clause; in the above example, we have two clauses, 𝑐1=𝑝1𝑝¯2𝑝3c1=p1∨p¯2∨p3 and 𝑐2=𝑝2𝑝5c2=p2∨p5. The disjuncts in a clause are called literals: for example, the first clause 𝑐1=𝑝1𝑝¯2𝑝3c1=p1∨p¯2∨p3 contains the literals 𝑝1p1𝑝¯2p¯2, and 𝑝3p3.

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:

𝑝1=𝑇𝑟𝑢𝑒,𝑝5=𝑇𝑟𝑢𝑒p1=True,p5=True

and any value for 𝑝2,𝑝3p2,p3.

## SAT representation

To represent an instance of SAT, we represent literals, clauses, and the overall expression, as follows.

Literals. We represent the literal 𝑝𝑘pk via the positive integer 𝑘k, and the literal 𝑝¯𝑘p¯k via the negative integer 𝑘−k.

Clauses. We represent a clause via the set of integers representing the clause literals.
For instance, we represent the clause 𝑝1𝑝¯3𝑝4p1∨p¯3∨p4 via the set {1,3,4}{1,−3,4}.

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

(𝑝1𝑝¯2𝑝3)(𝑝2𝑝5)(p1∨p¯2∨p3)∧(p2∨p5)

is represented by the set of sets:

{{1,2,3},{2,5}}.{{1,−2,3},{2,5}}.

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.

### Clauses

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.

### Truth assignments

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 to 𝑝𝑘pk via the integer 𝑘k, and the truth assignment that assigns False to 𝑝𝑘pk via 𝑘−k. Thus, if you have a (positive or negative) literal 𝑖i, the truth assignment 𝑖i 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 to 𝑝1p1 and False to 𝑝2p2 will be represented via the set {1,2}{1,−2}.

## 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 𝑐c (thus, 𝑐c is a set of integers) and a truth assignment 𝑖i (recall that 𝑖i can be positive or negative, depending on whether it assigns True or False to 𝑝𝑖pi). There are three cases:

• If 𝑖𝑐i∈c, then the 𝑖i literal of 𝑐c is true, and so is the whole clause. We return True to signify it.
• If 𝑖𝑐−i∈c, then the 𝑖−i literal of 𝑐c is false, and it cannot help make the clause true. We return the clause 𝑐{𝑖}c∖{−i}, which corresponds to the remaining ways of making the clause true under assignment 𝑖i.
• If neither 𝑖i nor 𝑖−i is in 𝑐c, then we return 𝑐c itself, as 𝑐c is not affected by the truth assignment 𝑖i.

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

#### 学本领，探索更大的世界！

error: Content is protected !!