Dichotomy theorem for generalized unique satisfiability problem (Q4934341)

In 1978 \textit{T. J. Schaefer} [``The complexity of satisfiability problems'', Conference Record of the 10th Annual ACM Symposium on Theory of Computing, 1978, 216-226 (1978)] examined the satisfiability problem for propositional formulas of the type ``conjunction of constraints'', where the constraints are arbitrary Boolean relations applied to a subset of the input variables. Lately, these satisfiability problems have become known under the name constraint satisfaction problems. Schaefer identified four classes of such formulas (Horn, anti-Horn, affine, and bijunctive) for which the satisfiability problem is polynomial-time solvable, and moreover he proved that in all other cases the satisfiability problem is NP-complete. Since then, a number of researchers have examined different types of satisfiability, counting, and optimization problems for Schaefer-type formulas. Theorems of the above structure are called dichotomy theorems (for particular satisfiability problems). In the present paper, the author examines the question if a given formula has exactly one satisfying assignment. Six classes of formulas are identified for which the problem is polynomial-time solvable, and it is shown that in all other cases the problem is coNP-hard (in fact, complete for the class US; see \textit{A. Blass} and \textit{Y. Gurevich} [Inf. Control 55, 80-88 (1982; Zbl 0543.03027)]). For the entire collection see [Zbl 0921.00033].