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: Main DPLL loop. Returns a generator of models.
  
  Variables are chosen successively, and assigned to be either
  True or False. If a solution is not found with this setting,
  the opposite is chosen and the search continues. The solver
  halts when every variable has a setting.
  
  Examples
  ========
  
  >>> from sympy.logic.algorithms.dpll2 import SATSolver
  >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
  ... {3, -2}], {1, 2, 3}, set())
  >>> list(l._find_model())
  [{1: True, 2: False, 3: False}, {1: True, 2: True, 3: True}]
  
  >>> from sympy.abc import A, B, C
  >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
  ... {3, -2}], {1, 2, 3}, set(), [A, B, C])
  >>> list(l._find_model())
  [{A: True, B: False, C: False}, {A: True, B: True, C: True}]
docstr_tok: ["Main","DPLL","loop",".","Returns","a","generator","of","models",".","Variables","are","chosen","successively",",","and","assigned","to","be","either","True","or","False",".","If","a","solution","is","not","found","with","this","setting",",","the","opposite","is","chosen","and","the","search","continues",".","The","solver","halts","when","every","variable","has","a","setting",".","Examples","========",">",">",">","from","sympy.logic.algorithms.dpll2","import","SATSolver",">",">",">","l","=","SATSolver","(","[","{","2",",","-3","}",",","{","1","}",",","{","3",",","-3","}",",","{","2",",","-2","}",",","...","{","3",",","-2","}","]",",","{","1",",","2",",","3","}",",","set","(",")",")",">",">",">","list","(","l._find_model","(",")",")","[","{","1",":","True",",","2",":","False",",","3",":","False","}",",","{","1",":","True",",","2",":","True",",","3",":","True","}","]",">",">",">","from","sympy.abc","import","A",",","B",",","C",">",">",">","l","=","SATSolver","(","[","{","2",",","-3","}",",","{","1","}",",","{","3",",","-3","}",",","{","2",",","-2","}",",","...","{","3",",","-2","}","]",",","{","1",",","2",",","3","}",",","set","(",")",",","[","A",",","B",",","C","]",")",">",">",">","list","(","l._find_model","(",")",")","[","{","A",":","True",",","B",":","False",",","C",":","False","}",",","{","A",":","True",",","B",":","True",",","C",":","True","}","]"]
code: def _find_model(self):
      """
      Main DPLL loop. Returns a generator of models.
  
      Variables are chosen successively, and assigned to be either
      True or False. If a solution is not found with this setting,
      the opposite is chosen and the search continues. The solver
      halts when every variable has a setting.
  
      Examples
      ========
  
      >>> from sympy.logic.algorithms.dpll2 import SATSolver
      >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
      ... {3, -2}], {1, 2, 3}, set())
      >>> list(l._find_model())
      [{1: True, 2: False, 3: False}, {1: True, 2: True, 3: True}]
  
      >>> from sympy.abc import A, B, C
      >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
      ... {3, -2}], {1, 2, 3}, set(), [A, B, C])
      >>> list(l._find_model())
      [{A: True, B: False, C: False}, {A: True, B: True, C: True}]
  
      """
  
      # We use this variable to keep track of if we should flip a
      #  variable setting in successive rounds
      flip_var = False
  
      # Check if unit prop says the theory is unsat right off the bat
      self._simplify()
      if self.is_unsatisfied:
          return
  
      # While the theory still has clauses remaining
      while True:
          # Perform cleanup / fixup at regular intervals
          if self.num_decisions % self.INTERVAL == 0:
              for func in self.update_functions:
                  func()
  
          if flip_var:
              # We have just backtracked and we are trying to opposite literal
              flip_var = False
              lit = self._current_level.decision
  
          else:
              # Pick a literal to set
              lit = self.heur_calculate()
              self.num_decisions += 1
  
              # Stopping condition for a satisfying theory
              if 0 == lit:
                  # check if assignment satisfies lra theory
                  if self.lra:
                      for enc_var in self.var_settings:
                          res = self.lra.assert_lit(enc_var)
                          if res is not None:
                              break
                      res = self.lra.check()
                      self.lra.reset_bounds()
                  else:
                      res = None
                  if res is None or res[0]:
                      yield {
                          self.symbols[abs(lit) - 1]: lit > 0
                          for lit in self.var_settings
                      }
                  else:
                      self._simple_add_learned_clause(res[1])
  
                  while self._current_level.flipped:
                      self._undo()
                  if len(self.levels) == 1:
                      return
                  flip_lit = -self._current_level.decision
                  self._undo()
                  self.levels.append(Level(flip_lit, flipped=True))
                  flip_var = True
                  continue
  
              # Start the new decision level
              self.levels.append(Level(lit))
  
          # Assign the literal, updating the clauses it satisfies
          self._assign_literal(lit)
  
          # _simplify the theory
          self._simplify()
  
          # Check if we've made the theory unsat
          if self.is_unsatisfied:
              self.is_unsatisfied = False
  
              # We unroll all of the decisions until we can flip a literal
              while self._current_level.flipped:
                  self._undo()
  
                  # If we've unrolled all the way, the theory is unsat
                  if 1 == len(self.levels):
                      return
  
              # Detect and add a learned clause
              self.add_learned_clause(self.compute_conflict())
  
              # Try the opposite setting of the most recent decision
              flip_lit = -self._current_level.decision
              self._undo()
              self.levels.append(Level(flip_lit, flipped=True))
              flip_var = True
  
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 4 for calling the SATSolver obj's underlying member method code with example usage: obj._find_model() without return types