博文
Solution k-CNF-SAT by The Remove Clause Counting Method
|||
Solution k-CNF-SAT by The Remove Clause Counting Method
Jiang Yongjiang
Email: accsys@126.com
Abstract:This paper presents a method for the remove clauses, which can be easily obtained from the total solution of k-CNF-SAT. This paper can prove NPC =P.
Keywords:NPC, P/NP problem, Count clause removed
1. The Count Clause Removed Algorithm
In this paper, we use the logical connectives are +(or),’(not), and the (and) connective is omitted.
We now give the followingspecial algorithm of Count clause removed.
(0) The establishment for n variables of one side symbols counter. like this x1’x2’x3’…xn-1’xn’[],x1’x2’x3’…xn-1’xn [],…, x1x2x3…xn-1xn []，total is 2n.
The every Counter initial value is 0.
(1) Remove all clause that has x and x’ in it. The remain clauses at most have 
.
Remove one clause and the counter plus one, if the k variables name in the clause belong to the counter name. For example clause is (x1+x2+x3) ,then the counter x1x2x3…xn-1xn [] plus 1.
(2) Final we can find which counter is 0, then the name symbol is xi,then xi=0. if is xi’,then xi=1.So we can get all solutions of the k-CNF-SAT.
(3) If non any counter is 0, the k-CNF cannot be equal to 1.
Example:f(x1,..., x6)= (x1+x1'+x2')(x2+x3+x4)(x1'+x3'+x4')(x1'+x2+x5')(x2+x3+x6)(x1+x5+x6'),please find out the satisfiable solutions.
Solution:
(0) The counters are x1’x2’x3’…x5’x6’[],x1’x2’x3’…x5’x6 [],…, x1x2x3…x5x6 []，and total is 64.
(1) Remove One-clause (x1+x1'+x2')，and the remains are
(x2+x3+x4)(x1'+x3'+x4')(x1'+x2+x5')(x2+x3+x6)(x1+x5+x6')
Clause (x2+x3+x4)can be plus 1 in counters x1x2x3…[1], (x1'+x3'+x4') can be plus 1 in counters
x1’ …x3’ x4’… [1],…, etc.
(2) Check all of the clause and then look at the counters.If a counter’s value is 0, the oppsite counter’s name is the solution. For instance,the counter x1’x2’x3 x4’x5’x6 [0] value is 0,then we have f(1,1,0,1,1, 0)=1.
2. Concepts and Properties
Way can we get all the solutions of the k-CNF=1 by the Count clause removed algorithm ?
Definition 1: if a clause has x and x’, then the clause is called a one-clause.
Definition 2: If a clause has x and is not one-clause,then it is called x-clause.
Definition 3: If we only have x or only have x’ the n variables word is called a One-side.
We can know there is 2n One-side.The counters are to record the number of clauses that are contained in One-side.
Theorem 1:One-side of n variables in k-CNF for the highest number of related clauses is 
.
Proof: becauseOne-side only have n variables, so get k≤n is .
Thus we know the counter’s maximum value is .
Definition 4:Remove clause ,that the one variable value is 1,it is called clause remove method in k-CNF.
Obviously,clause remove n times if there is not any remain clause,The k-CNF=1,otherwise it will be 0.
Theorem 2：k-CNF, there is not any One-clause,if remove x-clause connot remove x’-clause.
Proof: Because there is not any One-clause,so if we remove x-clause then we connot remove x’-clause.
Theorem 3：n variables k-CNF most have 
clauses, and One-clause maximum is
.
Definition 4: have clauses k-CNF is calld complete k-CNF.
Corollary: Complete k-CNF value of constant is 0.
Theorem 4：Any One-clause is not in k-CNF and if one One-side is not there ,then the k-CNF=1.
Proof:The x-clause contains all of the variables on one-side.If the one-side does not exist, it is determined that the opposite one-side remove thus there will not be any residual clause.
3. Conclusion
The Count clause removed algorithm is easy and simple method to the k-CNF-SAT. It is in polynomial time problem solving the k-CNF-SAT problem,so we can conclude NPC=P.
Original paper:http://blog.sciencenet.cn/blog-340399-905817.html
2015-7-17
https://blog.sciencenet.cn/blog-340399-906221.html
上一篇：寻找李斌网友
下一篇：问题求解与验证的区别，答柳渝之质疑
