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: Iterate over the various forms of propagation to simplify the theory.
  
  Examples
  ========
  
  >>> from sympy.logic.algorithms.dpll2 import SATSolver
  >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
  ... {3, -2}], {1, 2, 3}, set())
  >>> l.variable_set
  [False, False, False, False]
  >>> l.sentinels
  {-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
  
  >>> l._simplify()
  
  >>> l.variable_set
  [False, True, False, False]
  >>> l.sentinels
  {-3: {0, 2}, -2: {3, 4}, -1: set(), 2: {0, 3},
  ...3: {2, 4}}
docstr_tok: ["Iterate","over","the","various","forms","of","propagation","to","simplify","the","theory",".","Examples","========",">",">",">","from","sympy.logic.algorithms.dpll2","import","SATSolver",">",">",">","l","=","SATSolver","(","[","{","2",",","-3","}",",","{","1","}",",","{","3",",","-3","}",",","{","2",",","-2","}",",","...","{","3",",","-2","}","]",",","{","1",",","2",",","3","}",",","set","(",")",")",">",">",">","l.variable_set","[","False",",","False",",","False",",","False","]",">",">",">","l.sentinels","{","-3",":","{","0",",","2","}",",","-2",":","{","3",",","4","}",",","2",":","{","0",",","3","}",",","3",":","{","2",",","4","}","}",">",">",">","l._simplify","(",")",">",">",">","l.variable_set","[","False",",","True",",","False",",","False","]",">",">",">","l.sentinels","{","-3",":","{","0",",","2","}",",","-2",":","{","3",",","4","}",",","-1",":","set","(",")",",","2",":","{","0",",","3","}",",","...","3",":","{","2",",","4","}","}"]
code: def _simplify(self):
      """Iterate over the various forms of propagation to simplify the theory.
  
      Examples
      ========
  
      >>> from sympy.logic.algorithms.dpll2 import SATSolver
      >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
      ... {3, -2}], {1, 2, 3}, set())
      >>> l.variable_set
      [False, False, False, False]
      >>> l.sentinels
      {-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
  
      >>> l._simplify()
  
      >>> l.variable_set
      [False, True, False, False]
      >>> l.sentinels
      {-3: {0, 2}, -2: {3, 4}, -1: set(), 2: {0, 3},
      ...3: {2, 4}}
  
      """
      changed = True
      while changed:
          changed = False
          changed |= self._unit_prop()
          changed |= self._pure_literal()
  
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 10 for calling the SATSolver obj's underlying member method code with example usage: obj._simplify() without return types