Class SamplesManager

Class Documentation

class SamplesManager

Public Functions

SamplesManager(SampleSize num_samples, SolverConfiguration &config)

Initialize the sample manager. It creates complete blank samples.

void exportFinal(std::ostream &out, const DataAndStatistics &statistics, const SolverConfiguration &config)

Copy constructor. Equality operator.

Exports the set of samples to an output stream. This can be either a file or to the console.

Return
Reference to the new SamplesManager created. This allows for chaining equality operators. Sample Exporter
Parameters
  • other: Object to which the implicit object will be set.

Parameters
  • output_file_path: Path for export file
  • statistics: CNF and runtime statistics structure.
  • config: Solver configuration

void reservoirSample(const Component *active_comp, const std::vector<LiteralID> &literal_stack, const mpz_class &solution_weight, const mpz_class &weight_multiplier, const AltComponentAnalyzer &ana, VariableIndex literal_stack_ofs, const std::vector<VariableIndex> &freed_vars, const std::vector<CacheEntryID> &cached_comp_ids, const CachedAssignment &cached_assn, SampleAssignment &cached_sample)

Performs reservoir sampling

Parameters
  • active_comp: Currently active component.
  • literal_stack: Current assigned literal stack
  • sample_weight: Weight of the current set of samples to assign.

void GenerateSamplesToReplace(const mpz_class &new_sample_weight, std::vector<SampleSize> &samples_to_replace) const

Sample Replacement List Generator

Builds a list of the samples that will be replaced from the assignment collection. The selection of whether a sample will be replaced is based off their relative weighting of their sample counts.

Parameters
  • new_sample_weight: Model count weight for the new samples.
  • samples_to_replace: Contains the indices of the samples in the list that will be replaced.

void stitch(SamplesManager &other)

Sample Variable Assignment Accessor

Gets the value of the variable assignment for a specific sample in the list of samples

Debug function.

Stitches together to sample managers. This is used when combining the results after a component split.

Return
Variable’s assigned value. Samples Manager Stitcher
Parameters
  • sample_num: Sample number between 0 (inclusive) and num_samples (exclusive)
  • var: Variable number

Parameters

void StitchShuffledArray(SamplesManager &other)

Perform stitching permutation generation by creating a vector of size tot_num_samples_ (|S|) and shuffling it via a Fisher-Yates shuffle which has running time Theta(|S|).

Parameters

void SplitAndStitch(ListOfSamples::iterator &this_itr, ListOfSamples::iterator &other_itr, SampleSize &num_new_samples)

Splits the sample point to by this_itr. The new split sample has num_new_samples. This new sample is then stitched with the sample pointed to by other_itr. After performing the stitching, the sample count of other_itr is decreased by num_new_samples.

Note: that if num_new_samples and the sample count of this_itr are equal, the sample pointed to by this_itr is not split. All other steps proceed normally.

Parameters
  • this_itr: Sample to be split and then merged.
  • other_itr: Object that will be stitched with the new split sample.
  • num_new_samples: Sample size for the new stitched object. It must be greater than zero and less than or equal to the sample count of this_itr.

const bool verifyPostStitchingCorrectness(SamplesManager &other) const

Debug helper function to verify that post stitching, the number of samples is correct.

Return
True if the stitching appears correct.
Parameters
  • other: Set of samples that there were stitched to the implicit sample set.

void merge(SamplesManager &other, const mpz_class &other_multiplier, const std::vector<VariableIndex> &freed_vars, const std::vector<CacheEntryID> &cached_comp_ids, const CachedAssignment &cached_assn, SampleAssignment &cached_sample)

Samples Manager Merger

After a component split, a new descendant SamplesManager is created. This function will merge the existing SamplesManager with the original one before the component split.

See
other model count.
Parameters
  • other: Sample manager created for the descendants of the component split.
  • other_multiplier: Used to scale the model count of the
Parameters
  • freed_vars: List of emanicipated variables that can be set to either true or false.
  • cached_assn: Assignment stored in the cached that is used when storing samples in cache.
  • cached_sample: Sample output when performing sample caching. This will be used to update the top of the decision stack.

bool VerifySolutions(const std::string &input_file_path, bool skip_unassigned = false) const

Sample Verifier

Verifies that all samples generated by the program are valid and actually satisfies the input file. This is mostly for debug and should NEVER return false. If false is ever returned, something is wrong.

Return
true if all samples are valid.
Parameters
  • input_file_path: Path to a file in CNF formula
  • skip_unassigned: If true, skip verification of all clauses with an unassigned literal.

const mpz_class &model_count() const

Model Count Extractor

Gets the current number of solutions tracked by the manager object

Return
Model count for the samples manager object

void AddEmancipatedVars(const std::vector<VariableIndex> &emancipated_vars)

Emancipated and Unused Variable Adder

Unused variables are any variables that do not appear at all in a given formula. This sets them at the end of the countSAT execution.

Parameters
  • emancipated_vars: List of the IDs of unused variables.

void AddCachedCompIds(const std::vector<CacheEntryID> &cached_comp_ids)

Adds the specified cached component identification numbers to all samples in the collection.

Parameters
  • cached_comp_ids: Cached component identification numbers for all samples.

void TransferVariableAssignments(ListOfSamples &others)

Transfers the variable assignments from a previous sampler run and uses them to update the implicit sample manager. This is done when filling a partial assignment since multiple samples with the same cached component are run together even if the rest of their partial assignment is different.

Parameters
  • others: Existing samples from a previous solver run.

ListOfSamples &samples()

Solver Configuration Storer

This function is used to store a reference to the solver’s configuration. This is useful in case any of the run parameters are used.

Return
Reference to the sample managers recipe assignments.
Parameters
  • config: Solver’s configuration. Accessor to a sample manager’s variable assignment.

bool IsComplete() const

Sample Setter

This function replaces the sample (based off the specified number) with the new model passed to the function.

  • * Extracts a reference to the specified sample from the manager.
  • *
    Parameters
    • sample_num: Number of the sample to access - base 0
  • *
    Return
    Sample at the specified number Checks whether all the samples in the set are complete.
    Return
    true if all contained samples are complete.
Parameters
  • sample_num: Sample number to be set
  • new_model: New sample model to be stored Sample Accessor

void append(SamplesManager &other)

Adds the samples from one SamplesManager() to that of annother. This is different from merging and stitching as the implicit SamplesManager()’s samples remain unchanged. The only difference is the samples from other are appended to the collections of samples in the implicit parameter.

Parameters
  • other: Another SampleManager() object whose samples will be copied to the implicit parameter.

void append(ListOfSamples &other)

Adds the samples from one SamplesManager() to that of annother. This is different from merging and stitching as the implicit SamplesManager()’s samples remain unchanged. The only difference is the samples from other are appended to the collections of samples in the implicit parameter.

Parameters
  • other: A list of samples to add.

const SampleSize num_samples() const

Accessor for the number of samples actually stored by the SamplesManager() object.

Return
Number of samples actually stored by the SamplesManager().

void RemoveSamples(std::vector<SampleSize> &samples_to_remove)

Removes the samples specified at the indices in the samples_to_remove input.

Parameters
  • samples_to_remove: Identification numbers of the samples to remove.

void KeepSamples(std::vector<SampleSize> &samples_to_keep)

Specifies which samples from this SampleManager should be kept. All others are discarded. This is used as a compliment to the RemoveSamples() function since when there is a merge, one set keeps samples and the other discards them.

Parameters
  • samples_to_keep: Identification number of the samples that will be kept.

const bool verifySampleCount() const

Verifies that the SampleManager actually has the number of samples it is supposed to.

Return
True if the sample count is correct.

const SampleSize GetActualSampleCount() const

Gets the actual number of samples that are contained in this manager. In MOST (but not all) cases, this should equal the expected number of samples. However, that is not necessarily the case in some rare but useful exceptions.

Return
Actual number of samples contained in this object.

void clear()

Eliminate all existing samples.