Simplifying the propositional satisfiability problem by sub-model propagation ∗
Gábor Kusper, Lajos Cs H oke, Gergely Kovásznai · Acta Biologica Plantarum Agriensis (Eszterházy Károly University, Hungary) · 2008
We describes cases when we can simplify a general SAT problem instance by sub-model propagation. Assume that we test our input clause set whether it is blocked or not, because we know that a blocked clause set can be solved in polynomial time. If the input clause set is not blocked, but some clauses are blocked, then what can we do? Can we use the blocked clauses to simplify the clause set? The Blocked Clear Clause Rule and the Independent Blocked Clause Rule describe cases when the answer is yes. The other two independent clause rules, the Independent Nondecisive- and Independent Strongly Nondecisive Clause Rules describe cases when we can use nondecisive and strongly nondecisive clauses to simplify a general SAT problem instance.