=ADD=
=reftype=
14
=number=
02-02
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2002/02-02.ps.gz
=year=
2002
=month=
07
=author=
Kusper; Gabor
=title=
Solving the SAT Problem by Hyper-Unit Propagation
=abstract=
The SAT problem is the problem of finding a model for a formula in
conjunctive normal form. We developed two algorithms based on hyper-unit
propagation, which solve the SAT problem. Hyper-unit propagation is unit
propagation simultaneously by literals, as unit clauses, of an
assignment. The first method, called Unicorn-SAT algorithm, solves the
resolution-free SAT problem in linear time. A formula is resolution-free
if and only if there are no two clauses, which differ only in one
variable. For such a restricted formula we can find a model in linear time
by hyper-unit propagation. We obtain a sub-model, i.e., a part of the
model, by negation of a resolution-mate of a minimal clause, which is a
clause with the smallest number of literals in the formula. We obtain a
resolution-mate of a clause by negating one literal in it. By hyper-unit
propagation by a sub-model we obtain a formula, which has fewer variables
and clauses and remains resolution-free. Therefore, we can obtain a model
by joining the sub-models while we perform hyper-unit propagation by a
sub-model recursively until the formula becomes empty. The second method,
called General-Unicorn-SAT algorithm, solves the general SAT problem. The
algorithm is the same as Unicorn-SAT but in the general case this method
may result in an unsatisfiable formula, i.e., the Unicorn-SAT is not
complete for the genral SAT problem. To become complete we use
backtrack. If the obtained intermediate formula is unsatisfiable we
backtrack and we add the resolvent of the last chosen minimal clause and
its resolution-mate, which is the negation of the sub-model generated from
this minimal clause. This resolvent will be the minimal clause of the
formula. If this resolvent is the empty clause then we do backtrack
again. If it is not possible then the input problem is unsatisfiable. If
we reach the empty formula then the union of intermediate sub-models is a
model for the input problem. With this method, called General Unicorn-SAT,
we find a model for a formula if it is satisfiable or we detect if it is
unsatisfiable.
=sponsor=
RISC PhD scholarship program of the government of Upper Austria, FWF SFB F013 P1302, Austro-Hungarian Action Foundation