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: Perform unit propagation on the current theory.
docstr_tok: ["Perform","unit","propagation","on","the","current","theory","."]
code: def _unit_prop(self):
      """Perform unit propagation on the current theory."""
      result = len(self._unit_prop_queue) > 0
      while self._unit_prop_queue:
          next_lit = self._unit_prop_queue.pop()
          if -next_lit in self.var_settings:
              self.is_unsatisfied = True
              self._unit_prop_queue = []
              return False
          else:
              self._assign_literal(next_lit)
  
      return result
  
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 11 for calling the SATSolver obj's underlying member method code with example usage: obj._unit_prop() and returns: result, False