Class SamplesManager¶
- Defined in File model_sampler.h
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 filestatistics
: 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 stacksample_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
other
: Component split to be merged with.
-
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
other
: SamplesManager that will be stitched to the implicit SamplesManager.
-
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 hasnum_new_samples
. This new sample is then stitched with the sample pointed to byother_itr
. After performing the stitching, the sample count ofother_itr
is decreased bynum_new_samples
.Note: that if
num_new_samples
and the sample count ofthis_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 ofthis_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 formulaskip_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 setnew_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.
-