From: RussellE on 9 Mar 2010 23:37 I describe a method of classifying clauses in a 3SAT instance. One type of clause is always satisfiable in polynomial steps. Two other types of clauses are solvable in polynomial steps if certain conditions are met. Index set: a maximal set of independent clauses Index clause: a clause in the index set Index variable: a variable which appears in an index clause Non-Index variable: a variable that is not an index variable Two clauses are independent if they share no variables in common. A set of independent clauses is maximal if no more clauses in the instance can be added to the set. There is a simple algorithm for creating a maximal independent set of clauses: Choose a clause from the instance. Add this clause to the index set. Remove all clauses having a variable in common with this clause. Repeat this process on the remaining clauses until all clauses are removed. Every clause in a 3SAT instance can be uniquely classified with respect to an index set. Type 1: Clauses with 3 variables in common with an index clause. Type 2: Clauses with 2 variables in common with an index clause and 1 non-index variable. Type 3: Clauses with 1 variable in common with an index clause and 2 non-index variables. Type 4: Clauses with 1 variable in common with 2 different index clauses and 1 non-index variable. Type 5: Clauses with 2 variables in common with one index clause and 1 variable in common with another index clause. Type 6: Clauses with 1 variable in common with 3 different index clauses. I will refer to index clause families. An index clause family is the index clause and all type 1, 2, and 3 clauses which share variables in common with the index clause. An index clause family has no more than seven satisfying assignments. Type 1 clauses can be solved in a polynomial number of steps: 1) Find all satisfying assignments for the type 1 clauses in each index clause family. 2) An index clause family with eight type 1 clauses in unsatisfiable making the entire instance unsatisfiable. 3) Choose a satisfying assignment from each index clause family. The satisfying assignments for type 1 clauses in an index clause family form the "base formula". Type 1 clauses: (a+b+c)(~a+b+~c)(a+~b+~c) Base formula: a~b~c + ~ab~c + ab~c + ~a~bc + abc Each satisfying assignment either satisfies a type 2 clause or makes the type 2 clause a unit clause. The unit clause forces the assignment of a non-index variable. We can "extend" the base fomula with unit propagation of the type 2 clauses. Note, unit propogation may remove terms from the base formula. Type 2 clauses: (~a+~b+x)(a+c+y)(~a+b+x) Extended formula: a~b~c(x) + ~ab~c(y) + ab~c(x) + ~a~bc() + abc(x) We can reduce this formula by removing the base variables a,b, and c. These variables don't appear in any other type 1 or 2 clauses. Reduced formula: x + y + x + T + x = T Notice ~a~bc does not force the assignment of any non-index varibles. This means the reduced formula is a tautology. We can choose the assignment ~a~bc regardless of the assignments of the non-index variables. All type 1 and type 2 clauses can be solved in polynomial steps if the reduced formula for each index clause family has two or fewer variables. Assume the reduced formula for every index clause family is a tautology. 1) Choose an arbitrary assignment for the non-index variables. 2) For each index clause family, choose a satisfying assignment from the extended formula consistent with the assignment of non-index variables. There must be such an assignment if the reduced formula is a tautology. Assume the reduced formula for one or more index clause familys has two variables. The reduced formula does not have to be in CNF. If the reduced formula has no more than two variables, it can be converted into a CNF set of 2-clauses. We can AND the sets of 2-clauses from all the reduced formulas into a single 2SAT instance. If this 2SAT instance is unsatisfiable, the entire instance is unsatisfiable. Otherwise, we can take any satisfying assignment of the 2SAT instance and use the method desscibed above to find a satisfying assignment of the entire 3SAT instance. Similar arguments show combinations of type 1, type 2, and type 3 clauses can be solved in a polynomial number of steps if the reduced formula of every index clause family has two or fewer variables. Russell - 2 many 2 count