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: Initialize the data structures needed for the VSIDS heuristic.
docstr_tok: ["Initialize","the","data","structures","needed","for","the","VSIDS","heuristic","."]
code: def _vsids_init(self):
      """Initialize the data structures needed for the VSIDS heuristic."""
      self.lit_heap = []
      self.lit_scores = {}
  
      for var in range(1, len(self.variable_set)):
          self.lit_scores[var] = float(-self.occurrence_count[var])
          self.lit_scores[-var] = float(-self.occurrence_count[-var])
          heappush(self.lit_heap, (self.lit_scores[var], var))
          heappush(self.lit_heap, (self.lit_scores[-var], -var))
  
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 13 for calling the SATSolver obj's underlying member method code with example usage: obj._vsids_init() without return types