=ADD=
=reftype=
14
=number=
01-06
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2001/01-06.ps.gz
=year=
2001
=month=
02
=author=
Kusper; Gabor
=title=
Solving the Resolution-Free SAT Problem in Polynomial Time by Sub-Model Propagation
=abstract=
The SAT problem is the problem of finding a model for a clause set. It is
well known that the SAT problem is NP-complete on general clause sets. We
have developed a new method, called Unicorn-SAT algorithm, which solves
the SAT problem in polynomial time on resolution-free clause sets. A
clause set is resolution-free if and only if no resolution can be
performed on any two clauses of the clause set. For such a restricted
clause set, we can find a model in polynomial time by sub-model
propagation. We obtain the sub-model, i.e. a part of the model, by
Lucky-negation of that clause of the set which has the smallest number of
literals. Lucky-negation of a clause is the negation of all literals of
the clause except one. Sub-model propagation is unit propagation by each
literal of the sub-model. We obtain a model by joining the sub-models
while we perform sub-model propagation recursively until the clause set
becomes empty.
=note=
Conference paper 
=howpublished=
5th International Conference on Applied Informatics, Eger, Hungary, 28
January-3 February 2001
=sponsor=
European project Calculemus RTN1-1999-00301
=keywords=
SAT, resolution-free, sub-model, polynomial time