I have satisfiable 3SAT formula like:
(x1 or x2 or x3) and (not x1 or x2 or not x3)
and some clause which is not in this formula
(not x1 or x2 or x3).
Are there any methods to find out if this clause will turn formula in unsatisfiable state? Without obviously appending them and solving new formula. Or maybe some method to generate such type of clauses that won't affect satisfiability?
I am not necessarily looking for polynomial-time algorithms. But something better than brute force would be great. Probabilistic methods ideas are also welcome.