The SAT-UNSAT transition in the adversarial SAT problem

The study of random ensembles of decision problems has grown into a fertile field of investigation where the methods of statistical Physics have found applications to the theory (and practice) of hard combinatorial problems. This resulted in a wealth of intuition on the nature of the typical complexity of hard decision problems and in a new, efficient family of algorithms [1, 2]. One such problem is a random ensemble of satisfiability (in short SAT), where boolean formulas are generated in a random way and tested for a solution. If the formula is restricted to be of the form of a conjunction of an arbitrary number of clauses, and each clause is the logical disjunction of K variables, the problem is denoted by K-SAT. The ensemble is determined once the number of clauses per variable is fixed. As this ratio is increased the formulas go from being typically satisfiable to being typically unsatisfiable [2-4]. This is the SAT-UNSAT phase transition. Recent progress in the study of quantum decision problems [5] lead to the definition of the quantum generalisation of K-SAT (we call it K-QSAT) [6].