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","."]
code: def __init__(
      self,
      clauses,
      variables,
      var_settings,
      symbols=None,
      heuristic="vsids",
      clause_learning="none",
      INTERVAL=500,
      lra_theory=None,
  ):
      self.var_settings = var_settings
      self.heuristic = heuristic
      self.is_unsatisfied = False
      self._unit_prop_queue = []
      self.update_functions = []
      self.INTERVAL = INTERVAL
  
      if symbols is None:
          self.symbols = list(ordered(variables))
      else:
          self.symbols = symbols
  
      self._initialize_variables(variables)
      self._initialize_clauses(clauses)
  
      if "vsids" == heuristic:
          self._vsids_init()
          self.heur_calculate = self._vsids_calculate
          self.heur_lit_assigned = self._vsids_lit_assigned
          self.heur_lit_unset = self._vsids_lit_unset
          self.heur_clause_added = self._vsids_clause_added
  
          # Note: Uncomment this if/when clause learning is enabled
          # self.update_functions.append(self._vsids_decay)
  
      else:
          raise NotImplementedError
  
      if "simple" == clause_learning:
          self.add_learned_clause = self._simple_add_learned_clause
          self.compute_conflict = self.simple_compute_conflict
          self.update_functions.append(self.simple_clean_clauses)
      elif "none" == clause_learning:
          self.add_learned_clause = lambda x: None
          self.compute_conflict = lambda: None
      else:
          raise NotImplementedError
  
      # Create the base level
      self.levels = [Level(0)]
      self._current_level.varsettings = var_settings
  
      # Keep stats
      self.num_decisions = 0
      self.num_learned_clauses = 0
      self.original_num_clauses = len(self.clauses)
  
      self.lra = lra_theory
  
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 1 to create a new SATSolver object  with example: obj = SATSolver(clauses, variables, var_settings, symbols, heuristic, clause_learning, INTERVAL, lra_theory)