Class DataAndStatistics

Class Documentation

class DataAndStatistics

statistics.h

Purpose: Defines the DataAndStatistics() class.

Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.

Author
Zayd Hammoudeh zayd@ucsc.edu
Version
0.00.00

This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.

Original Author: Marc Thurley.

Public Functions

DataAndStatistics()
void UpdateNodeTypeStatistics(TopTreeNodeType node_type, const mpz_class &num_models)

Updates the number of nodes and total model count based on the top tree node type.

Parameters
  • node_type: Type of top tree node
  • num_models: Number of new models for the specified node type.

TreeNodeIndex num_tree_nodes(TopTreeNodeType node_type)

Accesor for the number of top tree nodes of a specified type.

Return
Total number of top tree nodes of the specified type.
Parameters
  • node_type: Type of top tree node.

mpz_class num_tree_node_models(TopTreeNodeType node_type)

Accessor for the total number of models associated with a specified type of top tree node.

Return
Total number of models associated with the specific top tree node type.
Parameters
  • node_type: Type of top tree node.

double percent_tree_node_models(TopTreeNodeType node_type)

Calculates the percentage of all models that are of a specific type.

Return
Percent of all models that fall under the specified node type
Parameters
  • node_type: Type of top tree node (e.g., cylinder, max depth, component split, etc.)

void reset_statistics()
bool cache_full() const

Checks whether the cache is full (i.e., exceeds 100% capacity).

Return
true if the cache is full and false otherwise.

uint64_t cache_bytes_memory_usage() const

Return
Sum of the infrastructure bytes and the sized of the cached components.

uint64_t overall_cache_bytes_memory_stored()
void incorporate_cache_store(CacheableComponent &ccomp)
void incorporate_cache_erase(CacheableComponent &ccomp)
void incorporate_cache_hit(CacheableComponent &ccomp)
unsigned long cache_MB_memory_usage()
double implicitBCP_miss_rate()
unsigned long num_clauses() const
unsigned long num_conflict_clauses()
unsigned long clause_deletion_interval()
void set_final_solution_count(const mpz_class &count)

Updates the solver field “final_solution_count_” with the solution count multiplied by 2^{#unused variables}. Hence:

final_solution_count_ = count * 2^(num_variables_ - num_used_variables_)

Parameters
  • count: model count.

const mpz_class &final_solution_count() const

Accessor for the final solution count

Return
Final solution count.

void incorporateClauseData(const std::vector<LiteralID> &clause)
void printShort()

statistics.cpp

Purpose: Defines methods for the DataAndStatistics() class.

Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.

Author
Zayd Hammoudeh zayd@ucsc.edu
Version
0.00.00

This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.

Original Author: Marc Thurley.

void printShortFormulaInfo()

Prints to the console information about the formula including: number of long, binary, & unit clauses, number of used variables, and total number of variables.

unsigned long getTime() const

Number of decisions (i.e., branch variable selections) made. This is used for determining when to remove components from the cache.

Return
Number of branch variable selections

long double getAvgComponentSize()
unsigned long cached_component_count()

Access the number of components in the cache.

Return

unsigned long cache_hits()

Number of cache look-ups where the component requested was in the cache.

Return
Cache look-up count.

double cache_miss_rate()

The rate of cache look-ups where the requested component was not in the cache.

Return
0 if a cache look-up never occurred. Otherwise, it is the number of caches misses divided by the total number of cache look-ups.

long double getAvgCacheHitSize()

The average size of a reused (i.e., hit) components in the cache.

Return
0 if a cache hit has never occurred. Otherwise, it is the average size of cached components that have ever been HIT.

Public Members

std::string input_file_

Path to the file containing the CNF formula used in the current run.

time_t start_time_
uint64_t maximum_cache_size_bytes_ = 0
SolverExitState exit_state_ = SolverExitState::NO_STATE
VariableIndex num_original_variables_ = 0
ClauseIndex num_original_clauses_ = 0
ClauseIndex num_original_binary_clauses_ = 0
ClauseIndex num_original_unit_clauses_ = 0
VariableIndex num_variables_ = 0

number of variables remaining

VariableIndex num_used_variables_ = 0

Number of variables that actually occurs in clauses

VariableIndex num_free_variables_ = 0

Number of variables that do not appear in any clause.

VariableIndex num_indep_support_variables_ = 0

Number of variables in the independent support.

ClauseIndex num_long_clauses_ = 0

Number of long clauses (i.e., greater than 3 unique literals) after pre-processing.

ClauseIndex num_binary_clauses_ = 0

Number of binary clauses after pre-processing.

ClauseIndex num_long_conflict_clauses_ = 0
ClauseIndex num_binary_conflict_clauses_ = 0
ClauseIndex times_conflict_clauses_cleaned_ = 0
ClauseIndex num_unit_clauses_ = 0
uint64_t num_decisions_ = 0

number of all decisions made - MT

Number of times a branch variable is set. It does not include BCP variable setting.

uint64_t num_failed_literals_detected_ = 0

Number of all failed literal detected.

uint64_t num_failed_literal_tests_ = 0
uint64_t num_conflicts_ = 0

Number of all conflicts encountered.

uint64_t num_clauses_learned_ = 0
VariableIndex max_component_split_depth_ = 0

Maximum number of embedded components splits.

VariableIndex max_branch_var_depth_ = 0

Maximum depth of branch variable setting. This excludes variables implied via UP or implied BCP.

TreeNodeIndex num_top_tree_nodes_ = 0

Number of top tree nodes observed.

TreeNodeIndex num_tree_nodes_by_type_[static_cast<long>(NUM_TREE_NODE_TYPES)]

Number of nodes of each of the top tree node types

mpz_class num_models_by_tree_node_type_[static_cast<long>(NUM_TREE_NODE_TYPES)]

Number of models for each of the top tree node types.

uint64_t num_cache_hits_ = 0
uint64_t num_cache_look_ups_ = 0
uint64_t sum_cache_hit_sizes_ = 0
uint64_t num_cached_components_ = 0
uint64_t sum_size_cached_components_ = 0
uint64_t sum_bytes_cached_components_ = 0

Number of bytes occupied by all cached components.

uint64_t overall_bytes_components_stored_ = 0
uint64_t sum_bytes_pure_cached_component_data_ = 0
uint64_t overall_bytes_pure_stored_component_data_ = 0
uint64_t sys_overhead_sum_bytes_cached_components_ = 0
uint64_t sys_overhead_overall_bytes_components_stored_ = 0
uint64_t cache_infrastructure_bytes_memory_usage_ = 0
uint64_t overall_num_cache_stores_ = 0
mpz_class final_solution_count_ = 0
double sampler_time_elapsed_ = DBL_MAX

Amount of time required to complete the full sampling.

double sampler_pass_1_time_ = DBL_MAX

Amount of time required to complete phase 1 and build all partial assignments (or just the time required to collect a single sample when two pass is disabled).

double sampler_pass_2_time_ = DBL_MAX

Time required to convert all partial assignments into complete assignments. This represents “pass 2” of the sampler.

std::vector<VariableIndex> numb_second_pass_vars_

When performing two pass testing, this records the number of variables that remain to be set at the start of the second pass for each sample.