let create (config: config) : state =
  let root_choice_point = {
    cp_id = 0;
    cp_split_literal = Term.null_literal;
    cp_right_splits = [];
    cp_valid = true;
  }
  in

  let state =
    {
      st_config = config;
      st_id = Counter.create_with 0;
      st_root_choice_point = root_choice_point;
      st_branch = [root_choice_point];
      st_literal_info = LiteralTable.create 1024;
    }
  in

  let root_branch_node = {
    li_literal = Term.null_literal;
    li_type = Propagation;
    li_choice_point = root_choice_point;
    li_context_unifier = Subst.empty;
    li_clause = [];
    li_clause_vars = [];
    li_clause_utility = (fun () -> ());
    li_clause_index = -2; (* just some number to crash on if ever used *)
    li_context_literals = [| |]; (* no dependency *)
    li_explanation = Some []; (* no explanation *)
  }
  in
    
    (* add special literals with no dependencies. *)
    LiteralTable.add state.st_literal_info Term.assert_literal root_branch_node;
    LiteralTable.add state.st_literal_info (Config.default_v state.st_config) root_branch_node;
    LiteralTable.add state.st_literal_info Term.null_literal root_branch_node;
    
    state