1 #include "link-includes.h" 2 3 #include "word-tag.hpp" 4 5 using namespace Minisat; 6 7 #ifdef HAVE_MKLIT 8 #define Lit(...) mkLit(__VA_ARGS__) 9 #endif 10 11 /** 12 * Base class for all SAT encodings 13 */ 14 class SATEncoder 15 { 16 public: 17 18 // Construct the encoder based on given sentence SATEncoder(Sentence sent,Parse_Options opts)19 SATEncoder(Sentence sent, Parse_Options opts) 20 : _variables(new Variables(sent)), _solver(new Solver()), 21 _opts(opts), _sent(sent) 22 { 23 _cost_cutoff = parse_options_get_disjunct_cost(opts); 24 25 verbosity = opts->verbosity; 26 debug = opts->debug; 27 test = opts->test; 28 29 // Preprocess word tags of the sentence 30 build_word_tags(); 31 } 32 ~SATEncoder()33 virtual ~SATEncoder() 34 { 35 delete _variables; 36 delete _solver; 37 } 38 39 // Create the formula from the sentence 40 void encode(); 41 42 // Solve the formula, returning the next linkage. 43 Linkage get_next_linkage(); 44 45 // Next linkage index in the linkage array 46 LinkageIdx _next_linkage_index = 0; 47 48 private: 49 int verbosity; 50 const char *debug; 51 const char *test; 52 53 protected: 54 55 /** 56 * Methods that generate various link-grammar constraints. 57 */ 58 59 // Top-level method that generates satisfaction conditions for every 60 // word in the sentence 61 void generate_satisfaction_conditions(); 62 63 // Generates satisfaction conditions for the word-tag expression e 64 void generate_satisfaction_for_expression(int w, int& dfs_position, Exp* e, char* var, 65 double parent_cost); 66 67 // Handle the case of NULL expression of a word 68 virtual void handle_null_expression(int w) = 0; 69 70 // Determine if this word-tag must be satisfied and generate appropriate clauses 71 virtual void determine_satisfaction(int w, char* name) = 0; 72 73 // Generates satisfaction condition for the connector (wi, pi) 74 virtual void generate_satisfaction_for_connector(int wi, int pi, 75 Exp* e, 76 char* var) = 0; 77 78 // Definition of link_cw((wi, pi), wj) variables when wj is an ordinary word 79 void generate_link_cw_ordinary_definition(size_t wi, int pi, 80 Exp* e, size_t wj); 81 82 // Generates order constraints for the elements of a conjunction. 83 void generate_conjunct_order_constraints(int w, Exp *e1, Exp* e2, int& dfs_position); 84 85 /** 86 * Methods used for optimizing conjunction ordering constraints 87 */ 88 89 // Number of connectors in an expression 90 int num_connectors(Exp* e); 91 92 // This expression can be matched without using any connectors of 93 // the given direction 94 static int empty_connectors(Exp* exp, char dir); 95 96 // This expression can be matched while using a connector of the 97 // given direction 98 static int non_empty_connectors(Exp* exp, char dir); 99 100 // Trailing connectors of a given direction in the given expression 101 void trailing_connectors(int w, Exp* exp, char dir, int& dfs_position, 102 std::vector<PositionConnector*>& connectors); 103 bool trailing_connectors_and_aux(int w, Exp* opd, char dir, int& dfs_position, 104 std::vector<PositionConnector*>& connectors); 105 106 // Connectors of the given direction that cannot be trailing 107 // connectors 108 void certainly_non_trailing(int w, Exp* exp, char dir, int& dfs_position, 109 std::vector<PositionConnector*>& connectors, bool has_right); 110 111 // Connectors that can act as leading connectors of a given 112 // direction in the given direction 113 void leading_connectors(int w, Exp* exp, char dir, int& dfs_position, 114 std::vector<PositionConnector*>& connectors); 115 116 /** 117 * Definitions of linked(wi, wj) variables. 118 */ 119 120 // Define all linked(wi, wj) variables 121 virtual void generate_linked_definitions() = 0; 122 123 // In order to reduce the number of clauses, some linked(wi, wj) 124 // variables can a priori be eliminated. The information about pairs 125 // of words that can be linked is kept in this matrix. 126 MatrixUpperTriangle<int> _linked_possible; 127 128 /** 129 * Planarity constraints 130 */ 131 132 // Generates clauses that forbid link-crossing 133 void generate_planarity_conditions(); 134 // Stronger planarity pruning 135 void generate_linked_min_max_planarity(); 136 137 138 /** 139 * Connectivity constraints 140 */ 141 142 #ifdef _CONNECTIVITY_ 143 // Generate clauses that encode the connectivity requirement of the 144 // linkage. Experiments showed that it is better to check the 145 // connectivity a posteriori and this method has been excised. 146 void generate_connectivity(); 147 #endif 148 149 150 // Helper method for connectivity_components 151 static void dfs(int node, const MatrixUpperTriangle<int>& graph, int component, std::vector<int>& components); 152 153 // Extract connectivity components of a linkage. Return true iff the linkage is connected. 154 bool connectivity_components(std::vector<int>& components); 155 156 // Generate clauses that prohibit all disconnected linkages that 157 // have the specified connectivity components. 158 void generate_disconnectivity_prohibiting(std::vector<int> components); 159 160 161 /** 162 * Encoding specific clauses - override to add clauses that are 163 * specific to a certain encoding 164 */ generate_encoding_specific_clauses()165 virtual void generate_encoding_specific_clauses() {} 166 167 168 /** 169 * Post-processing - PP pruning 170 * Generates PP pruning clauses. 171 */ 172 void pp_prune(); 173 174 175 /** 176 * Power pruning 177 */ 178 // Generate definition of epsilon variables that are used for power 179 // pruning 180 void generate_epsilon_definitions(); 181 bool generate_epsilon_for_expression(int w, int& dfs_position, Exp* e, char* var, bool root, char dir); 182 183 184 // Power pruning 185 void power_prune(); 186 // auxiliary method that extends power pruning clauses with additional literals 187 // (e.g., link should not be power-pruned if there words are fat-linked) add_additional_power_pruning_conditions(vec<Lit> & clause,int wl,int wr)188 virtual void add_additional_power_pruning_conditions(vec<Lit>& clause, int wl, int wr) 189 {} 190 191 // Cost cutoff threshold value. Nodes of the expression tree are 192 // pruned if their cost exceeds this value. Cost cutoff is performed 193 // during satisfaction condition generating. 194 double _cost_cutoff; 195 196 /** 197 * Creating clauses and passing them to the MiniSAT solver 198 */ 199 200 // Add the specified clause to the solver add_clause(vec<Lit> & clause)201 void add_clause(vec<Lit>& clause) { 202 #ifdef SAT_DEBUG 203 print_clause(clause); 204 #endif 205 for (int i = 0; i < clause.size(); i++) { 206 while (var(clause[i]) >= _solver->nVars()) { 207 _solver->newVar(); 208 } 209 } 210 _solver->addClause(clause); 211 } 212 213 214 // Print clause literals to standard output print_clause(const vec<Lit> & clause)215 static void print_clause(const vec<Lit>& clause) { 216 static int num = 1; 217 218 cout << "Clause: ." << num++ << ". "; 219 for (int i = 0; i < clause.size(); i++) 220 cout << (sign(clause[i]) ? '-' : '+') << var(clause[i]) << " "; 221 cout << endl; 222 } 223 224 225 226 /** 227 * Conversion of various formula types to CNF. Clauses obtained 228 * are automatically passed to the SAT Solver. 229 */ 230 void generate_literal(Lit l); 231 void generate_and_definition(Lit lhs, vec<Lit>& rhs); 232 void generate_or_definition(Lit lhs, vec<Lit>& rhs); 233 void generate_xor_definition(Lit lhs, vec<Lit>& rhs); 234 void generate_equivalence_definition(Lit l1, Lit l2); 235 void generate_classical_and_definition(Lit lhs, vec<Lit>& rhs); 236 void generate_and(vec<Lit>& vect); 237 void generate_or(vec<Lit>& vect); 238 void generate_xor_conditions(vec<Lit>& vect); 239 void generate_conditional_lr_implication_or_definition(Lit condition, Lit lhs, vec<Lit>& rhs); 240 void generate_conditional_lr_implication_or_definition(Lit condition1, Lit condition2, Lit lhs, vec<Lit>& rhs); 241 242 /* 243 * Word tags of the words in a sentence kept in a preprocessed 244 * form. This enables users to get information about the 245 * connectors in a very efficient way. 246 */ 247 // Word tags 248 std::vector<WordTag> _word_tags; 249 250 // Initializes _word_tags array 251 void build_word_tags(); 252 253 254 #if 0 255 // Find all matching connectors between two words 256 void find_all_matches_between_words(size_t w1, size_t w2, 257 std::vector<std::pair<const PositionConnector*, const PositionConnector*> >& matches); 258 259 // Check if the connector (wi, pi) can match any word in [l, r) 260 bool matches_in_interval(int wi, int pi, int l, int r); 261 #endif 262 263 264 // Join several expressions corresponding to different dictionary 265 // entries of a word into a single expression. 266 Exp* join_alternatives(int w); 267 268 /** 269 * Decoding 270 */ 271 272 // Convert propositional model to a parse info structure 273 virtual bool sat_extract_links(Linkage) = 0; 274 275 // Create linkage from a propositional model 276 bool create_linkage(Linkage); 277 278 // Generate clause that prohibits the current model 279 void generate_linkage_prohibiting(); 280 281 // Object that contains all information about the variable 282 // encoding. 283 Variables* _variables; 284 285 // The MiniSAT solver instance. The solver keeps the set of clauses. 286 Solver* _solver; 287 288 // Parse options. 289 Parse_Options _opts; 290 291 public: 292 // Sentence that is being parsed. 293 Sentence _sent; 294 295 /** 296 * Statistics. 297 */ 298 299 // Counters of main bottlenecks. 300 int _num_pp_violations = 0; // PP failures 301 int _num_lkg_disconnected = 0; // A disconnected linkage 302 303 // Print stats on solutions that have a performance impact. print_stats(void)304 void print_stats(void) 305 { 306 if (verbosity_level(D_USER_TIMES) || test_enabled("sat-stats")) 307 { 308 prt_error("Info: %d pp_violations, %d disconnected linkages.\n", 309 _num_pp_violations,_num_lkg_disconnected); 310 } 311 } 312 } 313 ; 314 315 316 /******************************************************************************* 317 * SAT encoding for sentences * 318 *******************************************************************************/ 319 class SATEncoderConjunctionFreeSentences : public SATEncoder 320 { 321 public: SATEncoderConjunctionFreeSentences(Sentence sent,Parse_Options opts)322 SATEncoderConjunctionFreeSentences(Sentence sent, Parse_Options opts) 323 : SATEncoder(sent, opts) { 324 #if 0 325 fprintf(stderr, "random_var_freq=%e\ngarbage_frac=%e\nclause_decay=%e\n" 326 "restart_first=%d\nvar_decay=%e\n", 327 _solver->random_var_freq, _solver->garbage_frac, _solver->clause_decay, 328 _solver->restart_first, _solver->var_decay); 329 330 _solver->random_var_freq = 0; 331 _solver->garbage_frac = 0.2; 332 _solver->clause_decay = 0.999; 333 _solver->restart_first = 100; 334 _solver->var_decay = 0.99; 335 #endif 336 337 verbosity = opts->verbosity; 338 debug = opts->debug; 339 test = opts->test; 340 } 341 342 virtual void handle_null_expression(int w); 343 virtual void determine_satisfaction(int w, char* name); 344 virtual void generate_satisfaction_for_connector(int wi, int pi, 345 Exp* e, 346 char* var); 347 348 349 virtual void generate_linked_definitions(); 350 virtual bool sat_extract_links(Linkage); 351 virtual Exp* PositionConnector2exp(const PositionConnector*); 352 353 virtual void generate_encoding_specific_clauses(); 354 355 private: 356 int verbosity; 357 const char *debug; 358 const char *test; 359 }; 360 361