How to determine if clause will change the satisfiability of the 3SAT formula?

Question

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.

Answer 1

The best you can do is append the clause and test satisfiability. There is no hope for anything better. (Proof: if there was a good method, then we could use it to solve 3SAT faster: if we had an arbitrary 3CNF formula $\varphi$, we could apply this method to a formula containing all but the last clause of $\varphi$ and the last clause of $\varphi$.)

Maybe what you really want to do is solve this problem repeatedly, with the same formula but a different clause. In other words, you want to test satisfiability of $\varphi \land c_1$, $\varphi \land c_2$, etc., where $\varphi$ is a 3CNF formula and each $c_i$ is a single clause. If so, some SAT solvers support the ability to "push" a clause and then "pop" it, exactly for this use case. This is sometimes known as "incremental solving". See, e.g., https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-incrementality, https://stackoverflow.com/q/18269016/781723. You could explore the literature to see what ideas they use for incremental solving.