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: Decay the VSIDS scores for every literal.
  
  Examples
  ========
  
  >>> from sympy.logic.algorithms.dpll2 import SATSolver
  >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
  ... {3, -2}], {1, 2, 3}, set())
  
  >>> l.lit_scores
  {-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
  
  >>> l._vsids_decay()
  
  >>> l.lit_scores
  {-3: -1.0, -2: -1.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -1.0}
docstr_tok: ["Decay","the","VSIDS","scores","for","every","literal",".","Examples","========",">",">",">","from","sympy.logic.algorithms.dpll2","import","SATSolver",">",">",">","l","=","SATSolver","(","[","{","2",",","-3","}",",","{","1","}",",","{","3",",","-3","}",",","{","2",",","-2","}",",","...","{","3",",","-2","}","]",",","{","1",",","2",",","3","}",",","set","(",")",")",">",">",">","l.lit_scores","{","-3",":","-2.0",",","-2",":","-2.0",",","-1",":","0.0",",","1",":","0.0",",","2",":","-2.0",",","3",":","-2.0","}",">",">",">","l._vsids_decay","(",")",">",">",">","l.lit_scores","{","-3",":","-1.0",",","-2",":","-1.0",",","-1",":","0.0",",","1",":","0.0",",","2",":","-1.0",",","3",":","-1.0","}"]
code: def _vsids_decay(self):
      """Decay the VSIDS scores for every literal.
  
      Examples
      ========
  
      >>> from sympy.logic.algorithms.dpll2 import SATSolver
      >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
      ... {3, -2}], {1, 2, 3}, set())
  
      >>> l.lit_scores
      {-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
  
      >>> l._vsids_decay()
  
      >>> l.lit_scores
      {-3: -1.0, -2: -1.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -1.0}
  
      """
      # We divide every literal score by 2 for a decay factor
      #  Note: This doesn't change the heap property
      for lit in self.lit_scores.keys():
          self.lit_scores[lit] /= 2.0
  
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 14 for calling the SATSolver obj's underlying member method code with example usage: obj._vsids_decay() without return types