1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #ifndef SOLVERCONF_H
24 #define SOLVERCONF_H
25
26 #include <string>
27 #include <vector>
28 #include <cstdlib>
29 #include <cassert>
30 #include "constants.h"
31 #include "cryptominisat5/solvertypesmini.h"
32
33 using std::string;
34
35 namespace CMSat {
36
37 enum class ClauseClean {
38 glue = 0
39 , activity = 1
40 };
41
clean_to_int(ClauseClean t)42 inline unsigned clean_to_int(ClauseClean t)
43 {
44 switch(t)
45 {
46 case ClauseClean::glue:
47 return 0;
48
49 case ClauseClean::activity:
50 return 1;
51 }
52
53 assert(false);
54 }
55
56 enum class PolarityMode {
57 polarmode_pos
58 , polarmode_neg
59 , polarmode_rnd
60 , polarmode_automatic
61 , polarmode_stable
62 , polarmode_best_inv
63 , polarmode_best
64 , polarmode_weighted
65 };
66
67 enum class Restart {
68 glue
69 , geom
70 , glue_geom
71 , luby
72 , never
73 };
74
getNameOfPolarmodeType(PolarityMode polarmode)75 inline std::string getNameOfPolarmodeType(PolarityMode polarmode)
76 {
77 switch(polarmode) {
78 case PolarityMode::polarmode_automatic :
79 return "auto";
80 case PolarityMode::polarmode_stable :
81 return "stb";
82 case PolarityMode::polarmode_best_inv :
83 return "ibst";
84 case PolarityMode::polarmode_best :
85 return "bst";
86 case PolarityMode::polarmode_neg :
87 return "neg";
88 case PolarityMode::polarmode_pos :
89 return "pos";
90 case PolarityMode::polarmode_weighted :
91 return "weighted";
92 case PolarityMode::polarmode_rnd :
93 return "rnd";
94 }
95 }
96
restart_type_to_short_string(const Restart type)97 inline std::string restart_type_to_short_string(const Restart type)
98 {
99 switch(type) {
100 case Restart::glue:
101 return "glue";
102
103 case Restart::geom:
104 return "geom";
105
106 case Restart::luby:
107 return "luby";
108
109 case Restart::glue_geom:
110 return "gl/g";
111
112 case Restart::never:
113 return "neve";
114 }
115
116 assert(false && "oops, one of the restart types has no string name");
117
118 return "ERR: undefined!";
119 }
120
polarity_mode_to_short_string(PolarityMode polarmode)121 inline std::string polarity_mode_to_short_string(PolarityMode polarmode)
122 {
123 switch(polarmode) {
124 case PolarityMode::polarmode_automatic :
125 return "auto";
126 case PolarityMode::polarmode_stable :
127 return "stb";
128 case PolarityMode::polarmode_best_inv :
129 return "istb";
130 case PolarityMode::polarmode_best :
131 return "bstb";
132 case PolarityMode::polarmode_neg :
133 return "neg";
134 case PolarityMode::polarmode_pos :
135 return "pos";
136 case PolarityMode::polarmode_weighted :
137 return "wght";
138 case PolarityMode::polarmode_rnd :
139 return "rnd";
140 }
141 }
142
getNameOfRestartType(Restart rest_type)143 inline std::string getNameOfRestartType(Restart rest_type)
144 {
145 switch(rest_type) {
146 case Restart::glue :
147 return "glue";
148
149 case Restart::geom:
150 return "geometric";
151
152 case Restart::glue_geom:
153 return "regularly switch between glue and geometric";
154
155 case Restart::luby:
156 return "luby";
157
158 case Restart::never:
159 return "never";
160
161 default:
162 assert(false && "Unknown clause cleaning type?");
163 }
164 }
165
getNameOfCleanType(ClauseClean clauseCleaningType)166 inline std::string getNameOfCleanType(ClauseClean clauseCleaningType)
167 {
168 switch(clauseCleaningType) {
169 case ClauseClean::glue :
170 return "glue";
171
172 case ClauseClean::activity:
173 return "activity";
174
175 default:
176 assert(false && "Unknown clause cleaning type?");
177 std::exit(-1);
178 }
179 }
180
181 class GaussConf
182 {
183 public:
184
GaussConf()185 GaussConf() :
186 autodisable(true)
187 , min_usefulness_cutoff(0.2)
188 , max_matrix_rows(5000)
189 , min_matrix_rows(3)
190 , max_num_matrices(5)
191 {
192 }
193
194 bool autodisable;
195 double min_usefulness_cutoff;
196 uint32_t max_matrix_rows; //The maximum matrix size -- no. of rows
197 uint32_t min_matrix_rows; //The minimum matrix size -- no. of rows
198 uint32_t max_num_matrices; //Maximum number of matrices
199
200 //Matrix extraction config
201 bool doMatrixFind = true;
202 uint32_t min_gauss_xor_clauses = 2;
203 uint32_t max_gauss_xor_clauses = 500000;
204 };
205
206 class DLL_PUBLIC SolverConf
207 {
208 public:
209 SolverConf();
210 std::string print_times(
211 const double time_used
212 , const bool time_out
213 , const double time_remain
214 ) const;
215 std::string print_times(
216 const double time_used
217 , const bool time_out
218 ) const;
219 std::string print_times(
220 const double time_used
221 ) const;
222
223 //Variable polarities
224 int do_lucky_polar_every_n;
225 PolarityMode polarity_mode;
226 int polar_stable_every_n;
227 int polar_best_inv_multip_n;
228 int polar_best_multip_n;
229
230 //Clause cleaning
231 float pred_short_size_mult;
232 float pred_long_size_mult;
233 float pred_forever_size_mult;
234 float pred_long_chunk_mult;
235 float pred_forever_chunk_mult;
236
237 //if non-zero, we reduce at every X conflicts.
238 //Reduced according to whether it's been used recently
239 //Otherwise, we *never* reduce
240 unsigned every_lev1_reduce;
241
242 //if non-zero, we reduce at every X conflicts.
243 //Otherwise we geometrically keep around max_temp_lev2_learnt_clauses*(inc**N)
244 unsigned every_lev2_reduce;
245
246 #if defined(FINAL_PREDICTOR) || defined(STATS_NEEDED)
247 unsigned every_lev3_reduce;
248 #endif
249
250 uint32_t must_touch_lev1_within;
251 unsigned max_temp_lev2_learnt_clauses;
252 double inc_max_temp_lev2_red_cls;
253
254 unsigned protect_cl_if_improved_glue_below_this_glue_for_one_turn;
255 unsigned glue_put_lev0_if_below_or_eq;
256 unsigned glue_put_lev1_if_below_or_eq;
257 double ratio_keep_clauses[2]; ///< Remove this ratio of clauses at every database reduction round
258 double clause_decay;
259
260 //If too many (in percentage) low glues after min_num_confl_adjust_glue_cutoff, adjust glue lower
261 double adjust_glue_if_too_many_low;
262 uint64_t min_num_confl_adjust_glue_cutoff;
263
264 //For restarting
265 unsigned restart_first; ///<The initial restart limit. (default 100)
266 double restart_inc; ///<The factor with which the restart limit is multiplied in each restart. (default 1.5)
267 Restart restartType; ///<If set, the solver will always choose the given restart strategy
268 int do_blocking_restart;
269 unsigned blocking_restart_trail_hist_length;
270 double blocking_restart_multip;
271
272 double local_glue_multiplier;
273 unsigned shortTermHistorySize; ///< Rolling avg. glue window size
274 unsigned lower_bound_for_blocking_restart;
275 double ratio_glue_geom; //higher the number, the more glue will be done. 2 is 2x glue 1x geom
276 int doAlwaysFMinim;
277
278 //Branch strategy
279 string branch_strategy_setup;
280
281 //Clause minimisation
282 int doRecursiveMinim;
283 int doMinimRedMore; ///<Perform learnt clause minimisation using watchists' binary and tertiary clauses? ("strong minimization" in PrecoSat)
284 int doMinimRedMoreMore;
285 unsigned max_glue_more_minim;
286 unsigned max_size_more_minim;
287 unsigned more_red_minim_limit_binary;
288 unsigned max_num_lits_more_more_red_min;
289
290 //Verbosity
291 int verbosity; ///<Verbosity level 0-2: normal 3+ extreme
292 int xor_detach_verb; ///to debug XOR detach issues
293
294 int doPrintGateDot; ///< Print DOT file of gates
295 int print_full_restart_stat;
296 int print_all_restarts;
297 int verbStats;
298 int do_print_times; ///Print times during verbose output
299 int print_restart_line_every_n_confl;
300
301 //Limits
302 double maxTime;
303 long max_confl;
304
305 //Glues
306 int update_glues_on_analyze;
307 uint32_t max_glue_cutoff_gluehistltlimited;
308
309 //chrono bt
310 int diff_declev_for_chrono;
311
312 //decision-based conflict clause generation
313 int do_decision_based_cl;
314 uint32_t decision_based_cl_max_levels;
315 uint32_t decision_based_cl_min_learned_size;
316
317 //SQL
318 bool dump_individual_restarts_and_clauses;
319 double dump_individual_cldata_ratio;
320 int sql_overwrite_file;
321 double lock_for_data_gen_ratio;
322
323 //Steps
324 double orig_step_size = 0.40;
325 double step_size_dec = 0.000001;
326 double min_step_size = 0.06;
327
328 //Var-elim
329 int doVarElim; ///<Perform variable elimination
330 uint64_t varelim_cutoff_too_many_clauses;
331 int do_empty_varelim;
332 int do_full_varelim;
333 long long empty_varelim_time_limitM;
334 long long varelim_time_limitM;
335 long long varelim_sub_str_limit;
336 double varElimRatioPerIter;
337 int skip_some_bve_resolvents;
338 int velim_resolvent_too_large; //-1 == no limit
339 int var_linkin_limit_MB;
340
341 //Subs, str limits for simplifier
342 long long subsumption_time_limitM;
343 double subsumption_time_limit_ratio_sub_str_w_bin;
344 double subsumption_time_limit_ratio_sub_w_long;
345 long long strengthening_time_limitM;
346
347 //Ternary resolution
348 bool doTernary;
349 long long ternary_res_time_limitM;
350 double ternary_keep_mult;
351 double ternary_max_create;
352 int allow_ternary_bin_create;
353
354 //Bosphorus
355 int do_bosphorus;
356 uint32_t bosphorus_every_n;
357
358 //BreakID
359 bool doBreakid;
360 bool breakid_use_assump; ///< If false breaks library use of solver
361 uint32_t breakid_every_n;
362 uint32_t breakid_vars_limit_K;
363 uint64_t breakid_cls_limit_K;
364 uint64_t breakid_lits_limit_K;
365 int64_t breakid_time_limit_K;
366 int breakid_max_constr_per_permut;
367 bool breakid_matrix_detect;
368
369 //BVA
370 int do_bva;
371 int min_bva_gain;
372 unsigned bva_limit_per_call;
373 int bva_also_twolit_diff;
374 long bva_extra_lit_and_red_start;
375 long long bva_time_limitM;
376 uint32_t bva_every_n;
377
378 //Probing
379 int doIntreeProbe;
380 int doTransRed; ///<carry out transitive reduction
381 unsigned long long intree_time_limitM;
382 unsigned long long intree_scc_varreplace_time_limitM;
383 int do_hyperbin_and_transred;
384
385 //XORs
386 int doFindXors;
387 unsigned maxXorToFind;
388 unsigned maxXorToFindSlow;
389 uint64_t maxXORMatrix;
390 uint64_t xor_finder_time_limitM;
391 int allow_elim_xor_vars;
392 unsigned xor_var_per_cut;
393 int force_preserve_xors;
394
395 //Cardinality
396 int doFindCard;
397
398 #ifdef FINAL_PREDICTOR
399 //Predictor system
400 std::string pred_conf_short;
401 std::string pred_conf_long;
402 std::string pred_conf_forever;
403 float pred_keep_above;
404 #endif
405
406 //Var-replacement
407 int doFindAndReplaceEqLits;
408 int max_scc_depth;
409
410 //Iterative Alo Scheduling
411 int simplify_at_startup; //simplify at 1st startup (only)
412 int simplify_at_every_startup; //always simplify at startup, not only at 1st startup
413 int do_simplify_problem;
414 int full_simplify_at_startup;
415 int never_stop_search;
416 uint64_t num_conflicts_of_search;
417 double num_conflicts_of_search_inc;
418 double num_conflicts_of_search_inc_max;
419 uint32_t max_num_simplify_per_solve_call;
420 string simplify_schedule_startup;
421 string simplify_schedule_nonstartup;
422 string simplify_schedule_preproc;
423
424 //Simplification
425 int perform_occur_based_simp;
426 int do_strengthen_with_occur; ///<Perform self-subsuming resolution
427 unsigned maxRedLinkInSize;
428 double maxOccurIrredMB;
429 double maxOccurRedMB;
430 double maxOccurRedLitLinkedM;
431 double subsume_gothrough_multip;
432
433 //Walksat
434 int doSLS;
435 uint32_t sls_every_n;
436 uint32_t yalsat_max_mems;
437 uint32_t sls_memoutMB;
438 uint32_t walksat_max_runs;
439 int sls_get_phase;
440 int sls_ccnr_asipire;
441 string which_sls;
442 uint32_t sls_how_many_to_bump;
443 uint32_t sls_bump_var_max_n_times;
444 uint32_t sls_bump_type;
445 int sls_set_offset;
446
447 //Distillation
448 int do_distill_clauses;
449 unsigned long long distill_long_cls_time_limitM;
450 long watch_based_str_time_limitM;
451 long long distill_time_limitM;
452 double distill_increase_conf_ratio;
453 long distill_min_confl;
454 double distill_red_tier1_ratio;
455
456 //Memory savings
457 int doRenumberVars;
458 int must_renumber; ///< if set, all "renumber" is treated as a "must-renumber"
459 int doSaveMem;
460 uint64_t full_watch_consolidate_every_n_confl;
461
462 //Component handling
463 int doCompHandler;
464 unsigned handlerFromSimpNum;
465 size_t compVarLimit;
466 unsigned long long comp_find_time_limitM;
467
468
469 //Misc Optimisations
470 int doStrSubImplicit;
471 long long subsume_implicit_time_limitM;
472 long long distill_implicit_with_implicit_time_limitM;
473
474 //Gates
475 int doGateFind; ///< Find OR gates
476 unsigned maxGateBasedClReduceSize;
477 int doShortenWithOrGates; ///<Shorten clauses with or gates during subsumption
478 int doRemClWithAndGates; ///<Remove clauses using and gates during subsumption
479 int doFindEqLitsWithGates; ///<Find equivalent literals using gates during subsumption
480 long long gatefinder_time_limitM;
481 long long shorten_with_gates_time_limitM;
482 long long remove_cl_with_gates_time_limitM;
483
484 //Gauss
485 GaussConf gaussconf;
486 bool doM4RI;
487 bool xor_detach_reattach;
488 bool force_use_all_matrixes;
489
490 //Sampling
491 std::vector<uint32_t>* sampling_vars;
492
493 //Timeouts
494 double orig_global_timeout_multiplier;
495 double global_timeout_multiplier;
496 double global_timeout_multiplier_multiplier;
497 double global_multiplier_multiplier_max;
498 double var_and_mem_out_mult;
499
500 //Multi-thread, MPI
501 unsigned long long sync_every_confl;
502 unsigned thread_num;
503
504 //Misc
505 unsigned origSeed;
506 unsigned reconfigure_val;
507 unsigned reconfigure_at;
508 unsigned preprocess;
509 int simulate_drat;
510 int conf_needed = true;
511 std::string simplified_cnf;
512 std::string solution_file;
513 std::string saved_state_file;
514 };
515
516 } //end namespace
517
518 #endif //SOLVERCONF_H
519