class_docstr: Class for representing a SAT solver capable of
   finding a model to a boolean theory in conjunctive
   normal form.
class_docstr_tok: ["Class","for","representing","a","SAT","solver","capable","of","finding","a","model","to","a","boolean","theory","in","conjunctive","normal","form","."]
docstr: Build a clause representing the fact that at least one decision made
  so far is wrong.
  
  Examples
  ========
  
  >>> from sympy.logic.algorithms.dpll2 import SATSolver
  >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
  ... {3, -2}], {1, 2, 3}, set())
  >>> next(l._find_model())
  {1: True, 2: False, 3: False}
  >>> l._simple_compute_conflict()
  [3]
docstr_tok: ["Build","a","clause","representing","the","fact","that","at","least","one","decision","made","so","far","is","wrong",".","Examples","========",">",">",">","from","sympy.logic.algorithms.dpll2","import","SATSolver",">",">",">","l","=","SATSolver","(","[","{","2",",","-3","}",",","{","1","}",",","{","3",",","-3","}",",","{","2",",","-2","}",",","...","{","3",",","-2","}","]",",","{","1",",","2",",","3","}",",","set","(",")",")",">",">",">","next","(","l._find_model","(",")",")","{","1",":","True",",","2",":","False",",","3",":","False","}",">",">",">","l._simple_compute_conflict","(",")","[","3","]"]
code: def _simple_compute_conflict(self):
      """Build a clause representing the fact that at least one decision made
      so far is wrong.
  
      Examples
      ========
  
      >>> from sympy.logic.algorithms.dpll2 import SATSolver
      >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
      ... {3, -2}], {1, 2, 3}, set())
      >>> next(l._find_model())
      {1: True, 2: False, 3: False}
      >>> l._simple_compute_conflict()
      [3]
  
      """
      return [-(level.decision) for level in self.levels[1:]]
  
imports: from collections import defaultdict
  from heapq import heappush, heappop
  from sympy.core.sorting import ordered
  from sympy.assumptions.cnf import EncodedCNF
  from sympy.logic.algorithms.lra_theory import LRASolver
label_desc: Use image node_id 20 for calling the SATSolver obj's underlying member method code with example usage: obj._simple_compute_conflict() and returns: unknown