Solving the resolution-free SAT problem by submodel propagation in linear time

摘要

We present a method, called Unicorn-SAT, based on submodel propagation, which solves the resolution-free SAT problem in linear time. A formula is resolution-free if there are no two clauses which differ only in one variable, i.e., each clause is blocked for each literal in it. A resolution-free formula is satisfiable or it contains the empty clause. For such a restricted formula we can find a model in linear time by submodel propagation. Submodel propagation is hyper-unit propagation by a submodel generated from a minimal clause. Hyper-unit propagation is unit propagation simultaneously by literals, as unit clauses, of a partial assignment. We obtain a submodel, i.e., a part of the model, by negation of a neighbor-resolution-mate of a minimal clause, which is a clause with the smallest number of literals in the formula. We obtain a neighbor-resolution-mate of a clause by negating one literal in it. By submodel propagation we obtain a formula which has fewer variables and clauses and remains resolution-free. Therefore, we can obtain a model by joining the submodels while we perform submodel propagation recursively until the formula becomes empty.