Dichotomy theorem for the generalized unique satisfiability problem

  • Laurent Juban
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


The unique satisfiability problem, that asks whether there exists a unique solution to a given propositional formula, was extensively studied in the recent years. This paper presents a dichotomy theorem for the unique satisfiability problem, partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases. We notice that the additional knowledge of a model makes this problem coNP-complete.We compare the polynomial cases of unique satisfiability to the polynomial cases of the usual satisfiability problem and show that they are incomparable. This difference between the polynomial cases is partially due to the necessity to apply parsimonious reductions among the unique satisfiability problems to preserve the number of solutions. In particular, we notice that the unique not-all-equal satisfiability problem, where we ask whether there is a unique model such that each clause has at least one true literal and one false literal, is solvable in polynomial time.


Polynomial Time Dichotomy Theorem Logical Relation Conjunctive Normal Form Truth Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BFS95]
    K. A. Berman, J. Franco, and J. S. Schlipf. Unique satisfiability of Horn sets can be solved in nearly linear time. Discrete Applied Mathematics, 60(1-3):77–91, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [BG82]
    A. Blass and Y. Gurevich. On the unique satisfiability problem. Information and Control, 55(1-3):80–88, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [CH96]
    N. Creignou and M. Hermann. Complexity of generalized satisfiability counting problems. Information and Computation, 125(1):1–12, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [CKR95]
    R. Chang, J. Kadin, and P. Rohatgi. On unique satisfiability and the thres-hold behavior of randomized reductions. Journal of Computer and System Science, 50(3):359–373, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [DG84]
    W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267–284, 1984.CrossRefMathSciNetzbMATHGoogle Scholar
  6. [GJ79]
    M. R. Garey and D. S. Johnson. Computers and intractability: A guide to the theory of NP-completeness. W.H. Freeman and Co, 1979.Google Scholar
  7. [HJ85]
    P. Hansen and B. Jaumard. Uniquely solvable quadratic Boolean equations. Discrete Applied Mathematics, 12(2):147–154, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [Koz92]
    D. C. Kozen. The design and analysis of algorithms, chapter 26: Counting problems and #P, pages 138–143. Springer-Verlag, 1992.Google Scholar
  9. [Min92]
    M. Minoux. The unique Horn-satisfiability problem and quadratic Boolean equations. Annals of Mathematics and Artificial Intelligence, 6(1-3):253–266, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  10. [Pap94]
    C. H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.Google Scholar
  11. [Pre93]
    D. Pretolani. A linear time algorithm for unique Horn satisfiability. Information Processing Letters, 48(2):61–66, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [Sch78]
    T. J. Schaefer. The complexity of satisfiability problems. In Proceedings 10th Symposium on Theory of Computing (STOC’78), San Diego (California, USA), pages 216–226, 1978.Google Scholar
  13. [VV86]
    L. G. Valiant and V. V. Vazirani. NP is as easy as detecting unique solutions. Theoretical Computer Science, 47(1):85–93, 1986.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Laurent Juban
    • 1
  1. 1.LORIA (Universitè Henri Poincarè Nancy 1)Vandœuvre-lèes-NancyFrance

Personalised recommendations