Proving Unsatisfiability

By applying a k-sat solver (and finding a solution) we can prove that a k-sat problem is satisfiable. For random 3-sat problems for instance this is expected to happen for m/n < 4.3 (m=nr. of clauses, n=nr. of variables). However, what if m/n > 4.3? In this case we expect that the problem is unsatisfiable but can we also prove it (so we can stop trying to solve it). There are algorithms for this too (although it seems to be a harder problem). Here is an easy one that I got from this website: .

Take a variable X that appears in the largest number of clauses and set it to FALSE. Now all clauses which contain "NOT X" are satisfied and all clauses which contain "X" have 2 variables left. Study the reduced problem with only these reduced 2-variable clauses which is a 2-sat (sub)problem of the original problem. 2-sat is solvable in polynomial time so it is easy to find out if solutions exist (or not), see and your homework Exercise 7.17. If no solutions exist, set "X=TRUE" and repeat. If again no solutions exist than there can be no solutions to the original 3-sat problem. If you cannot prove unsatisfiability for X move on to the next variable etc. If you can't prove unsatisfiability for any variables you fail...