link-grammar/sat-solver/sat-encoder.hpp

#include "link-includes.h"

#include "word-tag.hpp"

using namespace Minisat;

#ifdef HAVE_MKLIT
#define Lit(...) mkLit(__VA_ARGS__)
#endif

/**
 *    Base class for all SAT encodings
 */
class SATEncoder
{
public:

  // Construct the encoder based on given sentence
  SATEncoder(Sentence sent, Parse_Options  opts)
    : _variables(new Variables(sent)), _solver(new Solver()),
      _opts(opts), _sent(sent)
  {
    _cost_cutoff = parse_options_get_disjunct_cost(opts);

    verbosity = opts->verbosity;
    debug = opts->debug;
    test = opts->test;

    // Preprocess word tags of the sentence
    build_word_tags();
  }

  virtual ~SATEncoder()
  {
    delete _variables;
    delete _solver;
  }

  // Create the formula from the sentence
  void encode();

  // Solve the formula, returning the next linkage.
  Linkage get_next_linkage();

  // Next linkage index in the linkage array
  LinkageIdx _next_linkage_index = 0;

private:
  int verbosity;
  const char *debug;
  const char *test;

protected:

  /**
   *  Methods that generate various link-grammar constraints.
   */

  // Top-level method that generates satisfaction conditions for every
  // word in the sentence
  void generate_satisfaction_conditions();

  // Generates satisfaction conditions for the word-tag expression e
  void generate_satisfaction_for_expression(int w, int& dfs_position, Exp* e, char* var,
                                            double parent_cost);

  // Handle the case of NULL expression of a word
  virtual void handle_null_expression(int w) = 0;

  // Determine if this word-tag must be satisfied and generate appropriate clauses
  virtual void determine_satisfaction(int w, char* name) = 0;

  // Generates satisfaction condition for the connector (wi, pi)
  virtual void generate_satisfaction_for_connector(int wi, int pi,
                                                   Exp* e,
                                                   char* var) = 0;

  // Definition of link_cw((wi, pi), wj) variables when wj is an ordinary word
  void generate_link_cw_ordinary_definition(size_t wi, int pi,
                                            Exp* e, size_t wj);

  // Generates order constraints for the elements of a conjunction.
  void generate_conjunct_order_constraints(int w, Exp *e1, Exp* e2, int& dfs_position);

  /**
   *  Methods used for optimizing conjunction ordering constraints
   */

  // Number of connectors in an expression
  int num_connectors(Exp* e);

  // This expression can be matched without using any connectors of
  // the given direction
  static int  empty_connectors(Exp* exp, char dir);

  // This expression can be matched while using a connector of the
  // given direction
  static int  non_empty_connectors(Exp* exp, char dir);

  // Trailing connectors of a given direction in the given expression
  void trailing_connectors(int w, Exp* exp, char dir, int& dfs_position,
                           std::vector<PositionConnector*>& connectors);
  bool trailing_connectors_and_aux(int w, Exp* opd, char dir, int& dfs_position,
                                   std::vector<PositionConnector*>& connectors);

  // Connectors of the given direction that cannot be trailing
  // connectors
  void certainly_non_trailing(int w, Exp* exp, char dir, int& dfs_position,
                              std::vector<PositionConnector*>& connectors, bool has_right);

  // Connectors that can act as leading connectors of a given
  // direction in the given direction
  void leading_connectors(int w, Exp* exp, char dir, int& dfs_position,
                          std::vector<PositionConnector*>& connectors);

  /**
   *  Definitions of linked(wi, wj) variables.
   */

  // Define all linked(wi, wj) variables
  virtual void generate_linked_definitions() = 0;

  // In order to reduce the number of clauses, some linked(wi, wj)
  // variables can a priori be eliminated. The information about pairs
  // of words that can be linked is kept in this matrix.
  MatrixUpperTriangle<int> _linked_possible;

  /**
   *  Planarity constraints
   */

  // Generates clauses that forbid link-crossing
  void generate_planarity_conditions();
  // Stronger planarity pruning
  void generate_linked_min_max_planarity();


  /**
   *  Connectivity constraints
   */

#ifdef _CONNECTIVITY_
  // Generate clauses that encode the connectivity requirement of the
  // linkage. Experiments showed that it is better to check the
  // connectivity a posteriori and this method has been excised.
  void generate_connectivity();
#endif


  // Helper method for connectivity_components
  static void dfs(int node, const MatrixUpperTriangle<int>& graph, int component, std::vector<int>& components);

  // Extract connectivity components of a linkage. Return true iff the linkage is connected.
  bool connectivity_components(std::vector<int>& components);

  // Generate clauses that prohibit all disconnected linkages that
  // have the specified connectivity components.
  void generate_disconnectivity_prohibiting(std::vector<int> components);


  /**
   *   Encoding specific clauses - override to add clauses that are
   *   specific to a certain encoding
   */
  virtual void generate_encoding_specific_clauses() {}


  /**
   *   Post-processing - PP pruning
   *   Generates PP pruning clauses.
   */
  void pp_prune();


  /**
   *   Power pruning
   */
  // Generate definition of epsilon variables that are used for power
  // pruning
  void generate_epsilon_definitions();
  bool generate_epsilon_for_expression(int w, int& dfs_position, Exp* e, char* var, bool root, char dir);


  // Power pruning
  void power_prune();
  // auxiliary method that extends power pruning clauses with additional literals
  // (e.g., link should not be power-pruned if there words are fat-linked)
  virtual void add_additional_power_pruning_conditions(vec<Lit>& clause, int wl, int wr)
  {}

  // Cost cutoff threshold value. Nodes of the expression tree are
  // pruned if their cost exceeds this value. Cost cutoff is performed
  // during satisfaction condition generating.
  double _cost_cutoff;

  /**
   *   Creating clauses and passing them to the MiniSAT solver
   */

  // Add the specified clause to the solver
  void add_clause(vec<Lit>& clause) {
#ifdef SAT_DEBUG
    print_clause(clause);
#endif
    for (int i = 0; i < clause.size(); i++) {
      while (var(clause[i]) >= _solver->nVars()) {
        _solver->newVar();
      }
    }
    _solver->addClause(clause);
  }


  // Print clause literals to standard output
  static void print_clause(const vec<Lit>& clause) {
    static int num = 1;

    cout << "Clause: ." << num++ << ". ";
    for (int i = 0; i < clause.size(); i++)
      cout << (sign(clause[i]) ? '-' : '+') << var(clause[i]) << " ";
    cout << endl;
  }


  /**
   *   Conversion of various formula types to CNF. Clauses obtained
   *   are automatically passed to the SAT Solver.
   */
  void generate_literal(Lit l);
  void generate_and_definition(Lit lhs, vec<Lit>& rhs);
  void generate_or_definition(Lit lhs, vec<Lit>& rhs);
  void generate_xor_definition(Lit lhs, vec<Lit>& rhs);
  void generate_equivalence_definition(Lit l1, Lit l2);
  void generate_classical_and_definition(Lit lhs, vec<Lit>& rhs);
  void generate_and(vec<Lit>& vect);
  void generate_or(vec<Lit>& vect);
  void generate_xor_conditions(vec<Lit>& vect);
  void generate_conditional_lr_implication_or_definition(Lit condition, Lit lhs, vec<Lit>& rhs);
  void generate_conditional_lr_implication_or_definition(Lit condition1, Lit condition2, Lit lhs, vec<Lit>& rhs);

  /*
   *   Word tags of the words in a sentence kept in a preprocessed
   *   form. This enables users to get information about the
   *   connectors in a very efficient way.
   */
  // Word tags
  std::vector<WordTag> _word_tags;

  // Initializes _word_tags array
  void build_word_tags();


#if 0
  // Find all matching connectors between two words
  void find_all_matches_between_words(size_t w1, size_t w2,
                                      std::vector<std::pair<const PositionConnector*, const PositionConnector*> >& matches);

  // Check if the connector (wi, pi) can match any word in [l, r)
  bool matches_in_interval(int wi, int pi, int l, int r);
#endif


  // Join several expressions corresponding to different dictionary
  // entries of a word into a single expression.
  Exp* join_alternatives(int w);

  /**
   * Decoding
   */

  // Convert propositional model to a parse info structure
  virtual bool sat_extract_links(Linkage) = 0;

  // Create linkage from a propositional model
  bool create_linkage(Linkage);

  // Generate clause that prohibits the current model
  void generate_linkage_prohibiting();

  // Object that contains all information about the variable
  // encoding.
  Variables* _variables;

  // The MiniSAT solver instance. The solver keeps the set of clauses.
  Solver* _solver;

  // Parse options.
  Parse_Options  _opts;

public:
  // Sentence that is being parsed.
  Sentence _sent;

  /**
   * Statistics.
   */

  // Counters of main bottlenecks.
  int _num_pp_violations = 0;    // PP failures
  int _num_lkg_disconnected = 0; // A disconnected linkage

  // Print stats on solutions that have a performance impact.
  void print_stats(void)
  {
    if (verbosity_level(D_USER_TIMES) || test_enabled("sat-stats"))
    {
      prt_error("Info: %d pp_violations, %d disconnected linkages.\n",
                _num_pp_violations,_num_lkg_disconnected);
    }
  }
}
;


/*******************************************************************************
 *       SAT encoding for sentences                                            *
 *******************************************************************************/
class SATEncoderConjunctionFreeSentences : public SATEncoder
{
public:
  SATEncoderConjunctionFreeSentences(Sentence sent, Parse_Options  opts)
    : SATEncoder(sent, opts) {
#if 0
    fprintf(stderr, "random_var_freq=%e\ngarbage_frac=%e\nclause_decay=%e\n"
           "restart_first=%d\nvar_decay=%e\n",
           _solver->random_var_freq, _solver->garbage_frac, _solver->clause_decay,
           _solver->restart_first, _solver->var_decay);

    _solver->random_var_freq = 0;
    _solver->garbage_frac = 0.2;
    _solver->clause_decay = 0.999;
    _solver->restart_first = 100;
    _solver->var_decay = 0.99;
#endif

    verbosity = opts->verbosity;
    debug = opts->debug;
    test = opts->test;
  }

  virtual void handle_null_expression(int w);
  virtual void determine_satisfaction(int w, char* name);
  virtual void generate_satisfaction_for_connector(int wi, int pi,
                                                   Exp* e,
                                                   char* var);


  virtual void generate_linked_definitions();
  virtual bool sat_extract_links(Linkage);
  virtual Exp* PositionConnector2exp(const PositionConnector*);

  virtual void generate_encoding_specific_clauses();

private:
  int verbosity;
  const char *debug;
  const char *test;
};