@Article{Fellner2,
  author =       "Andreas Fellner and Pascal Fontaine and Bruno
                 Woltzenlogel Paleo",
  title =        "{NP}-completeness of small conflict set generation for
                 congruence closure",
  journal =      "Formal Methods in System Design",
  year =         "2017",
  ISSN =         "1572-8102",
  abstract =     "The efficiency of satisfiability modulo theories (SMT)
                 solvers is dependent on the capability of theory
                 reasoners to provide small conflict sets, i.e. small
                 unsatisfiable subsets from unsatisfiable sets of
                 literals. Decision procedures for uninterpreted symbols
                 (i.e. congruence closure algorithms) date back from the
                 very early days of SMT. Nevertheless, to the best of
                 our knowledge, the complexity of generating smallest
                 conflict sets for sets of literals with uninterpreted
                 symbols and equalities had not yet been determined,
                 although the corresponding decision problem was
                 believed to be NP-complete. We provide here an
                 NP-completeness proof, using a simple reduction from
                 SAT.",
  month =        dec,
  day =          "01",
  volume =       "51",
  number =       "3",
  pages =        "533--544",
  URL =          "Fellner2.pdf",
}