Program Listing for File solver.h

↰ Return to documentation for file (src/solver.h)

#ifndef SOLVER_H_
#define SOLVER_H_

#include <sys/time.h>

#include <algorithm>
#include <utility>
#include <vector>
#include <string>

#include "statistics.h"
#include "instance.h"
#include "component_management.h"

#include "solver_config.h"
#include "model_sampler.h"
#include "cached_assignment.h"
//#include "top_tree_sampler.h"


class StopWatch {
 public:
  StopWatch();
  bool timeBoundBroken() {
    timeval actual_time = (struct timeval) {0};
    gettimeofday(&actual_time, nullptr);
    return actual_time.tv_sec - start_time_.tv_sec > time_bound_;
  }

  bool start() {
    auto ret = static_cast<bool>(gettimeofday(&last_interval_start_, nullptr));
    start_time_ = stop_time_ = last_interval_start_;
    return !ret;
  }
  bool stop() {
    return gettimeofday(&stop_time_, nullptr) == 0;
  }

  double getElapsedSeconds() {
    timeval r = getElapsedTime();
    return r.tv_sec + static_cast<double>(r.tv_usec) / 1000000;
  }

  bool interval_tick() {
    timeval actual_time = (struct timeval) {0};
    gettimeofday(&actual_time, nullptr);
    if (actual_time.tv_sec - last_interval_start_.tv_sec
        > interval_length_.tv_sec) {
      gettimeofday(&last_interval_start_, nullptr);
      return true;
    }
    return false;
  }

  void setTimeBound(uint64_t seconds) {
    time_bound_ = seconds;
  }
  // ZH Appears to neither be implemented or used.
  //long int getTimeBound();

 private:
  timeval start_time_;
  timeval stop_time_;

  uint64_t time_bound_ = UINT64_MAX;

  timeval interval_length_;
  timeval last_interval_start_;

  timeval getElapsedTime();
};

class Solver: public Instance {
 public:
  Solver(int argc, char *argv[]);

  Solver(SolverConfiguration &config, DataAndStatistics &statistics,
         SampleSize num_samples = 0, bool two_pass = true)
      : config_(config), final_samples_(num_samples, config_) {
    LinkConfigAndStatistics();

    statistics_.input_file_ = statistics.input_file_;

    // ToDo modify to support caching multiple samples
    //config_.num_samples_to_cache_ = num_samples;
    config_.num_samples_to_cache_ = 1;
    sampler_stopwatch_.setTimeBound(config_.time_bound_seconds);  // Initialize the time bound.
    config_.samples_output_file = "";

    config_.disable_samples_write_ = true;
    config_.num_samples_ = num_samples;
    time(&statistics_.start_time_);
    config_.perform_two_pass_sampling_ = two_pass;
  }
  Solver(const Solver &other)
      : config_(other.config_), final_samples_(other.final_samples_.num_samples(), config_) {
    // Bring over the configuration and statistics
    statistics_ = other.statistics_;
    LinkConfigAndStatistics();
    config_.num_samples_to_cache_ = 1;
    config_.disable_samples_write_ = true;

    // Data structures used in the createFromFile Function
    literal_pool_ = other.literal_pool_;
    variables_ = other.variables_;
    literal_values_ = other.literal_values_;
    unit_clauses_ = other.unit_clauses_;
    unused_vars_ = other.unused_vars_;

    independent_support = other.independent_support;
    has_independent_support_ = other.has_independent_support_;
    conflict_clauses_ = other.conflict_clauses_;
    occurrence_lists_ = other.occurrence_lists_;
    literals_ = other.literals_;

    // Initialize other variables as needed
    statistics_.start_time_ = other.statistics_.start_time_;  // Needed to ensure timeout
    sampler_stopwatch_.setTimeBound(config_.time_bound_seconds);  // Initialize the time bound.
    original_lit_pool_size_ = other.original_lit_pool_size_;
  }
  void solve(const PartialAssignment &partial_assn = PartialAssignment());
  void sample_models();
  const SolverConfiguration &config() {
    return config_;
  }
  void DisableTopTreeSampling() {
    assert(config_.perform_top_tree_sampling);
    config_.perform_top_tree_sampling = false;
  }
  const DataAndStatistics &statistics() {
    return statistics_;
  }
  void PushNewSamplesManagerOnStack() {
    if (config_.store_sampled_models())
      samples_stack_.emplace_back(SamplesManager(config_.num_samples_, config_));
  }
//  /**
//   * Literal Stack Location Printer
//   *
//   * Debug only tool.  Often, a CNF formula has hundreds of thousands
//   * of variables on the literal stack.  Finding where a specific variable
//   * is on the stack (if at all) can be time consuming.  This function
//   * prints whether the specified variable is on the stack.
//   *
//   * @param var Variable number of interest.
//   */
//  void PrintLiteralStackLocation(VariableIndex var);

  //  End Sampler Objects

 private:
  SolverConfiguration config_;
  DecisionStack stack_;
  std::vector<LiteralID> literal_stack_;
  ComponentManager comp_manager_ = ComponentManager(config_, statistics_, literal_values_);
  StopWatch sampler_stopwatch_;
  uint64_t last_ccl_deletion_time_ = 0;
  uint64_t last_ccl_cleanup_time_ = 0;
  std::vector<SamplesManager> samples_stack_;
  SamplesManager final_samples_;
  bool simplePreProcess();

  bool prepFailedLiteralTest();
  void reservoir_sample_models(const PartialAssignment &partial_assn, Solver &temp_solver);
//  /**
//   * MT - we assert that the formula is consistent and has not been
//   * found UNSAT yet hard wires all assertions in the literal stack
//   * into the formula removes all set variables and essentially
//   * reinitializes all further data.
//   */
//  void HardWireAndCompact();
  SolverExitState countSAT();
  void decideLiteral();
  bool bcp();
  void decayActivitiesOf(Component & comp) {
    for (auto it = comp.varsBegin(); *it != varsSENTINEL; it++) {
      literal(LiteralID(*it, true)).activity_score_ *=0.5;
      literal(LiteralID(*it, false)).activity_score_ *=0.5;
    }
  }
  bool implicitBCP();
  bool BCP(VariableIndex start_at_stack_ofs);
  SolverNextAction backtrack();
  void ProcessCacheStore();
  void ProcessSampleComponentSplitBacktrack();
  SolverNextAction resolveConflict();
  void PrintFinalSamplerResults();

  //  BEGIN small helper functions

  float scoreOf(VariableIndex v) {
    float score = comp_manager_.scoreOf(v);
    score += 10.0 * literal(LiteralID(v, true)).activity_score_;
    score += 10.0 * literal(LiteralID(v, false)).activity_score_;
//    score += (10*stack_.get_decision_level()) * literal(LiteralID(v, true)).activity_score_;
//    score += (10*stack_.get_decision_level()) * literal(LiteralID(v, false)).activity_score_;
    return score;
  }
  bool setLiteralIfFree(LiteralID lit, Antecedent ant = Antecedent(NOT_A_CLAUSE)) {
    if (literal_values_[lit] != X_TRI)
      return false;
    var(lit).decision_level = stack_.get_decision_level();
    var(lit).ante = ant;
    literal_stack_.push_back(lit);
    if (ant.isAClause() && ant.asCl() != NOT_A_CLAUSE)
      getHeaderOf(ant.asCl()).increaseScore();
    literal_values_[lit] = T_TRI;
    literal_values_[lit.neg()] = F_TRI;
    return true;
  }
  void printOnlineStats();
//  /**
//   * Literal Stack Contents Checker
//   *
//   * Checks whether the specified variable is in the literal stack.
//   *
//   * @param var Variable of interest
//   * @return true if the specified variable @see var is in the literal stack.
//   */
//  bool IsVarInLiteralStack(VariableIndex var);

  void setConflictState(LiteralID litA, LiteralID litB) {
    violated_clause.clear();
    violated_clause.push_back(litA);
    violated_clause.push_back(litB);
  }

  void setConflictState(ClauseOfs cl_ofs) {
    getHeaderOf(cl_ofs).increaseScore();
    violated_clause.clear();
    for (auto it = beginOf(cl_ofs); *it != SENTINEL_LIT; it++)
      violated_clause.push_back(*it);
  }

  std::vector<LiteralID>::const_iterator TOSLiteralsBegin() {
    return literal_stack_.begin() + stack_.top().literal_stack_ofs();
  }
  void initStack(unsigned long resSize = 0) {
    stack_.clear();
    if (resSize != 0)
      stack_.reserve(resSize);
    literal_stack_.clear();
    if (resSize != 0)
      literal_stack_.reserve(resSize);
    // initialize the stack to contain at least level zero
    stack_.push_back(StackLevel(1, 0, 2));
    stack_.back().changeBranch();
    // Reset the samples stack.
    if (config_.store_sampled_models()) {
      samples_stack_.clear();
      samples_stack_.reserve(30);
    }
    set_variable_depth_ = 0;
    statistics_.max_component_split_depth_ = 0;
  }

  const LiteralID &TOS_decLit() const {
    assert(stack_.top_const().literal_stack_ofs() < literal_stack_.size());
    return literal_stack_[stack_.top_const().literal_stack_ofs()];
  }
  void reactivateTOS() {
    for (auto it = TOSLiteralsBegin(); it != literal_stack_.end(); it++)
      unSet(*it);
    comp_manager_.cleanRemainingComponentsOf(stack_.top());
    literal_stack_.resize(stack_.top().literal_stack_ofs());
    stack_.top().resetRemainingComps();
  }

  bool fail_test(LiteralID lit) {
    VariableIndex sz = literal_stack_.size();
    // we increase the decLev artificially
    // s.t. after the tentative BCP call, we can learn a conflict clause
    // relative to the assn_ of *jt
    stack_.startFailedLitTest();
    setLiteralIfFree(lit);

    assert(!hasAntecedent(lit));

    bool bSucceeded = BCP(sz);
    if (!bSucceeded)
      recordAllUIPCauses();

    stack_.stopFailedLitTest();

    while (literal_stack_.size() > sz) {
      unSet(literal_stack_.back());
      literal_stack_.pop_back();
    }
    return bSucceeded;
  }
  //  BEGIN conflict analysis

  // if the state name is CONFLICT,
  // then violated_clause contains the clause determining the conflict;
  std::vector<LiteralID> violated_clause;
  // this is an array of all the clauses found
  // during the most recent conflict analysis
  // it might contain more than 2 clauses
  // but always will have:
  //      uip_clauses_.front() the 1UIP clause found
  //      uip_clauses_.back() the lastUIP clause found
  //  possible clauses in between will be other UIP clauses
  std::vector<std::vector<LiteralID>> uip_clauses_;

  // the assertion level of uip_clauses_.back()
  // or (if the decision variable did not have an antecedent
  // before) then assertionLevel_ == DL;
  int64_t assertion_level_ = 0;

  // build conflict clauses from most recent conflict
  // as stored in state_.violated_clause
  // solver state must be CONFLICT to work;
  // this first method record only the last UIP clause
  // so as to create clause that asserts the current decision
  // literal
  void recordLastUIPCauses();
  void recordAllUIPCauses();

  void minimizeAndStoreUIPClause(LiteralID uipLit,
                                 std::vector<LiteralID> & tmp_clause,
                                 const bool seen[]);

  // Commented out by ZH as not implemented
//  void storeUIPClause(LiteralID uipLit, std::vector<LiteralID> & tmp_clause);

//  int getAssertionLevel() const {
//    return assertion_level_;
//  }

  //  END conflict analysis

  VariableIndex set_variable_depth_ = 0;
  bool InitializeSolverAndPreprocess(const PartialAssignment &partial_assn);

  void applyPartialAssignment(const PartialAssignment &partial_assn);
  void ReportSharpSatResults();
  void PerformInitialSampling();
  inline void FillPartialAssignments(Solver &temp_solver);
  inline bool IsEndSamplesStackSizeValid() const {
    return samples_stack_.size() == 1
           || (samples_stack_.size() == 2 && samples_stack_[0].model_count() == 0);
  }
//  /**
//   * Checks whether the current point in the solver execution is valid for storing a top
//   * tree sample.
//   *
//   * @return true If there none of the current literal assignments led to a component split,
//   * the current depth is below the maximum and top tree mode is enabled.
//   */
//  inline bool IsValidTopTreeNodeStorePoint() {
//    return config_.perform_top_tree_sampling && set_variable_depth_ < config_.max_top_tree_depth_;
//  }
  inline void LinkConfigAndStatistics() {
    // ToDo If the solver is multithreaded, static for config and statistics will need to change.
    StackLevel::set_solver_config_and_statistics(config_, statistics_);
//    SamplesManager::set_solver_config(config_);
  }
};

#endif // SOLVER_H_