I have a set of clauses S. I know how the Linear Resolution Principle algorithm can find the unsatisfiability of the set , but i dont understand how it finds if the the set is satisfable. How it happens ?
ps: is it somehow connected to the fact that the input resolution algorithm is incomplete ?
It is not completeness.
We have the Completeness of the Resolution Principle:
The issue is about undecidability of FOL: there are formulas that are satisfiable only in infinite domains.
When we apply the resolution proof procedure, we have three possible cases: if the procedure halts without producing the empty clause, then the set $S$ is satisfiable. If $S$ is unsatisfiable, the procedure halts with the empty clause.
If, on the other hand, $S$ is satisfiable only in an infinite domain, then the procedure does not halt.
Thus, if we can not deduce the empty clause from $S$, then the set $S$ is not unsatisfiable, i.e. it is satisfiable.