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 #include "constants.h"
24 #include "solverconf.h"
25 #include <limits>
26 #include <iomanip>
27 #include <sstream>
28 using namespace CMSat;
29
30 //UPDATEs for DEVEL
31 //Fixing to:
32 //1832701 out-9660847.wlm01-4 239 147 92 a54ed65 --simdrat 1 --bva 1 --slsgetphase 1 --slstype ccnr_yalsat --confbtwsimp 70000 --confbtwsimpinc 1.1 --modbranchstr 3
33 //sat race 2019
34 //2049104 out-9833438.wlm01-7-drat0 220 135 85 c975a55 --simdrat 1 --slseveryn 2 --slstype ccnr --bvalim 150000 --tern 1 --terncreate 1 --ternkeep 6 -m 3 --distillincconf 0.04 --distillminconf 20000
35
36
37 //UPDATEs for MASTER
38 //1830735 out-9839185.wlm01-8-drat0 243 148 95 2a30cfb
39 //--simdrat 1 --bva 1 --slstype ccnr --slseveryn 2 --bvalim 250000 --tern 1 --terncreate 1 --ternkeep 6 -m 3 --distillincconf 0.02 --distillminconf 10000 --slsgetphase 1
40
41 //Fixing to:
42 //--simdrat 1 --bva 1 --slstype ccnr --slseveryn 2 --bvalim 250000 --tern 1 --terncreate 1 --ternkeep 6 -m 3 --distillincconf 0.02 --distillminconf 10000 --slsgetphase 1 --slstobump 100 --gluehist 60 --diffdeclevelchrono 20 --conftochrono 0
43
44 //Fixing to:
45 //1722973 out-9860239.wlm01-1-drat0 254 154 100 a6005cf --simdrat 1 --gluehist 50 --moremoreminim 1 --lev1usewithin 70000 --bva2lit 1
46
47 //Fixing to:
48 //1838305 out-9882018.wlm01-1-drat0 241 145 96 16de7b4 --simdrat 1 --substimelimbinratio 0.1 --substimelimlongratio 0.9 --distilltier1ratio 0.03 --sublonggothrough 1.0 --varelimto 750 --bvaeveryn 7
49
50 //Fixing to:
51 //1706988 out-9885914.wlm01-6-drat0 253 153 100 def3339 --simdrat 1 --vsidsalternate 1 --vsidsalterval1 0.92 --vsidsalterval2 0.99 --maplealternate 1 --maplealterval1 0.70 --maplealterval2 0.90
52
53 //NOTE: diffdeclevel 0 is not good
54 //1813642 out-9896604.wlm01-0-drat0 242 146 96 6d8c7e2 _satcomp2020 --simdrat 1
55 //1867880 out-9896604.wlm01-1-drat0 237 139 98 6d8c7e2 _satcomp2020 --simdrat 1 --diffdeclevelchrono 0
56
57 //XOR is good, even on GAUSS
58 //1755046 out-9896604.wlm01-8-drat0 250 146 104 edd5be7 _devel --xor 1 --breakid 1 --breakideveryn 5
59 //1773691 out-9896604.wlm01-13-drat0 247 144 103 edd5be7 _devel --xor 0 --breakid 1 --breakideveryn 5
60
61 //Tuning to
62 //1684592 out-9915739.wlm01-3-drat0 256 149 107 b3b7cfb _devel --printsol 0 --xorfindtout 400 --gaussusefulcutoff 0.2
63
64 //Tuning to
65 //1732414 out-9915739.wlm01-7-drat0 254 157 97 b3b7cfb _devel --printsol 0 --simdrat 1 --polarstablen 4
66
67 //Tuning to
68 //1713867 out-175744.wlm01-11-drat0 252 154 98 de15a43 _devel --printsol 0 --simdrat 1 --slsbumptype 6 --polarbestinvmult 9 --lucky 20
69
SolverConf()70 DLL_PUBLIC SolverConf::SolverConf() :
71 do_lucky_polar_every_n(20)
72 , polarity_mode(PolarityMode::polarmode_automatic)
73 , polar_stable_every_n(4)
74 , polar_best_inv_multip_n(9)
75 , polar_best_multip_n(1000)
76
77 //Clause cleaning
78 , pred_short_size_mult(0.5)
79 , pred_long_size_mult(0.5)
80 , pred_forever_size_mult(0.25)
81 , pred_long_chunk_mult(1.0)
82 , pred_forever_chunk_mult(1.0)
83
84 , every_lev1_reduce(10000) // kept for a while then moved to lev2
85 , every_lev2_reduce(15000) // cleared regularly
86 #if defined(FINAL_PREDICTOR) || defined(STATS_NEEDED)
87 , every_lev3_reduce(10000)
88 #endif
89 , must_touch_lev1_within(70000)
90
91 , max_temp_lev2_learnt_clauses(30000) //only used if every_lev2_reduce==0
92 , inc_max_temp_lev2_red_cls(1.0) //only used if every_lev2_reduce==0
93 , protect_cl_if_improved_glue_below_this_glue_for_one_turn(30)
94 #ifdef FINAL_PREDICTOR
95 , glue_put_lev0_if_below_or_eq(0)
96 , glue_put_lev1_if_below_or_eq(0)
97 #else
98 , glue_put_lev0_if_below_or_eq(3) // never removed
99 , glue_put_lev1_if_below_or_eq(6) // kept for a while then moved to lev2
100 #endif
101 , clause_decay(0.999)
102
103 , adjust_glue_if_too_many_low(0.7)
104 , min_num_confl_adjust_glue_cutoff(150ULL*1000ULL)
105 //NOTE: The "Scavel" system's "usedt" does NOT speed up the solver
106 //test conducted: out-drat-check-8359337.wlm01-1-drat0
107
108 //Restarting
109 , restart_first(100)
110 , restart_inc(1.1)
111 , restartType(Restart::glue_geom)
112 , do_blocking_restart(1)
113 , blocking_restart_trail_hist_length(5000)
114 , blocking_restart_multip(1.4)
115 , local_glue_multiplier(0.80)
116 , shortTermHistorySize (50)
117 , lower_bound_for_blocking_restart(10000)
118 , ratio_glue_geom(5)
119 , doAlwaysFMinim(false)
120
121 //branch strategy
122 , branch_strategy_setup("maple1+maple2+vsids2+maple1+maple2+vsids1")
123
124 //Clause minimisation
125 , doRecursiveMinim (true)
126 , doMinimRedMore(true)
127 , doMinimRedMoreMore(true)
128 , max_glue_more_minim(6)
129 , max_size_more_minim(30)
130 , more_red_minim_limit_binary(200)
131 , max_num_lits_more_more_red_min(1)
132
133 //Verbosity
134 , verbosity (0)
135 , xor_detach_verb (0)
136 , doPrintGateDot (false)
137 , print_full_restart_stat (false)
138 , print_all_restarts (false)
139 , verbStats (1)
140 , do_print_times(1)
141 , print_restart_line_every_n_confl(8192)
142
143 //Limits
144 , maxTime (std::numeric_limits<double>::max())
145 , max_confl (std::numeric_limits<long>::max())
146
147 //Glues
148 , update_glues_on_analyze(true)
149 #ifdef FINAL_PREDICTOR
150 , max_glue_cutoff_gluehistltlimited(100000)
151 #else
152 , max_glue_cutoff_gluehistltlimited(50)
153 #endif
154
155 //Chono BT
156 , diff_declev_for_chrono (20)
157
158 //decision-based clause generation. These values have been validated
159 //see 8099966.wlm01
160 , do_decision_based_cl(1)
161 , decision_based_cl_max_levels(9)
162 , decision_based_cl_min_learned_size(50)
163
164 //SQL
165 , dump_individual_restarts_and_clauses(true)
166 , dump_individual_cldata_ratio(0.01)
167 , sql_overwrite_file(0)
168 , lock_for_data_gen_ratio(0.1)
169
170 //Var-elim
171 , doVarElim (true)
172 , varelim_cutoff_too_many_clauses(2000)
173 , do_empty_varelim (true)
174 , do_full_varelim(true)
175 , empty_varelim_time_limitM(300LL)
176 , varelim_time_limitM(750)
177 , varelim_sub_str_limit(600)
178 , varElimRatioPerIter(1.60)
179 , skip_some_bve_resolvents(true) //based on gates
180 , velim_resolvent_too_large(20)
181 , var_linkin_limit_MB(1000)
182
183 //Subs, str limits for simplifier
184 , subsumption_time_limitM(300)
185 , subsumption_time_limit_ratio_sub_str_w_bin(0.1)
186 , subsumption_time_limit_ratio_sub_w_long(0.9)
187 , strengthening_time_limitM(300)
188
189
190 //Ternary resolution
191 #ifdef FINAL_PREDICTOR
192 , doTernary(false)
193 #else
194 , doTernary(true)
195 #endif
196 , ternary_res_time_limitM(100)
197 , ternary_keep_mult(6)
198 , ternary_max_create(1)
199 , allow_ternary_bin_create(false)
200
201 //Bosphorus
202 , do_bosphorus(false)
203 , bosphorus_every_n(1)
204
205 //BreakID
206 , doBreakid(true)
207 , breakid_use_assump(true)
208 , breakid_every_n(5)
209 , breakid_vars_limit_K(300)
210 , breakid_cls_limit_K(600)
211 , breakid_lits_limit_K(3500)
212 , breakid_time_limit_K(2000)
213 , breakid_max_constr_per_permut(50)
214 , breakid_matrix_detect(true)
215
216 //Bounded variable addition
217 , do_bva(true)
218 , min_bva_gain(32)
219 , bva_limit_per_call(250000)
220 , bva_also_twolit_diff(true)
221 , bva_extra_lit_and_red_start(0)
222 , bva_time_limitM(50)
223 , bva_every_n(7)
224
225 //Probing
226 , doIntreeProbe (true)
227 , doTransRed (true)
228 , intree_time_limitM(1200ULL)
229 , intree_scc_varreplace_time_limitM(30ULL)
230 , do_hyperbin_and_transred(true)
231
232 //XOR
233 , doFindXors (true)
234 , maxXorToFind (7)
235 , maxXorToFindSlow (5)
236 , maxXORMatrix (400ULL)
237 , xor_finder_time_limitM(400)
238 , allow_elim_xor_vars(1)
239 , xor_var_per_cut(2)
240 , force_preserve_xors(false)
241
242 //Cardinality
243 , doFindCard(0)
244
245 #ifdef FINAL_PREDICTOR
246 //Predict system
247 , pred_conf_short("../../src/predict/predictor_short.json")
248 , pred_conf_long("../../src/predict/predictor_long.json")
249 , pred_conf_forever("../../src/predict/predictor_forever.json")
250 , pred_keep_above(0.5f)
251 #endif
252
253 //Var-replacer
254 , doFindAndReplaceEqLits(true)
255 , max_scc_depth (10000)
256
257 //Iterative Alo Scheduling
258 , simplify_at_startup(false)
259 , simplify_at_every_startup(false)
260 , do_simplify_problem(true)
261 , full_simplify_at_startup(false)
262 , never_stop_search(false)
263 , num_conflicts_of_search(50ULL*1000ULL)
264 , num_conflicts_of_search_inc(1.4)
265 , num_conflicts_of_search_inc_max(10)
266 , max_num_simplify_per_solve_call(25)
267 , simplify_schedule_startup(
268 "sub-impl,"
269 "breakid, "
270 "occ-backw-sub-str, occ-clean-implicit, occ-bve,"
271 "occ-ternary-res, occ-backw-sub-str, occ-xor, "
272 "card-find,"
273 "cl-consolidate," //consolidate after OCC
274 "scc-vrepl,"
275 "sub-cls-with-bin,"
276 "bosphorus,"
277 "sls,lucky"
278 )
279
280 //validated with run 8114195.wlm01
281 , simplify_schedule_nonstartup(
282 "handle-comps,"
283 "scc-vrepl,"
284 "sub-impl,"
285 "intree-probe,"
286 "sub-str-cls-with-bin,distill-cls,"
287 "scc-vrepl,sub-impl,str-impl,sub-impl,"
288 "breakid,"
289 //occurrence based
290 "occ-backw-sub-str,occ-clean-implicit,occ-bve,"//occ-gates,"
291 "occ-bva,occ-ternary-res,occ-xor,card-find,"
292 //consolidate after OCC
293 "cl-consolidate,"
294 //strengthen again
295 "str-impl,sub-str-cls-with-bin,distill-cls,"
296 "scc-vrepl,"
297 //renumber then it's time for SLS
298 "renumber,"
299 "bosphorus,"
300 "sls,lucky"
301 )
302 , simplify_schedule_preproc(
303 "handle-comps,"
304 "scc-vrepl,"
305 "sub-impl,"
306 "sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,"
307 "breakid, "
308 "occ-backw-sub-str, occ-clean-implicit, occ-bve, occ-bva,"
309 "occ-ternary-res, occ-xor,"
310 //"occ-gates,"
311 "cl-consolidate," //consolidate after OCC
312 "str-impl, sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,"
313 "str-impl, sub-impl, sub-str-cls-with-bin,"
314 "intree-probe, "
315 "must-renumber"
316 )
317
318 //Occur based simplification
319 , perform_occur_based_simp(true)
320 , do_strengthen_with_occur (true)
321 , maxRedLinkInSize (200)
322 , maxOccurIrredMB (2500)
323 , maxOccurRedMB (600)
324 , maxOccurRedLitLinkedM(50)
325 , subsume_gothrough_multip(1.0)
326
327 //WalkSAT
328 , doSLS(true)
329 , sls_every_n(2)
330 , yalsat_max_mems(40)
331 , sls_memoutMB(500)
332 , walksat_max_runs(50)
333 , sls_get_phase(1)
334 , sls_ccnr_asipire(1)
335 , which_sls("ccnr")
336 , sls_how_many_to_bump(100)
337 , sls_bump_var_max_n_times(100)
338 , sls_bump_type(6)
339 , sls_set_offset(0)
340
341 //Distillation
342 , do_distill_clauses(true)
343 , distill_long_cls_time_limitM(20ULL)
344 , watch_based_str_time_limitM(30LL)
345 , distill_time_limitM(120LL)
346 , distill_increase_conf_ratio(0.02)
347 , distill_min_confl(10000)
348 , distill_red_tier1_ratio(0.03)
349
350 //Memory savings
351 , doRenumberVars (true)
352 , must_renumber (false)
353 , doSaveMem (true)
354 , full_watch_consolidate_every_n_confl (4ULL*1000ULL*1000ULL) //validated in run 8113323.wlm01
355
356 //Component finding
357 , doCompHandler (false)
358 , handlerFromSimpNum (0)
359 , compVarLimit (1ULL*1000ULL*1000ULL)
360 , comp_find_time_limitM (500)
361
362 //Misc optimisations
363 , doStrSubImplicit (true)
364 , subsume_implicit_time_limitM(100LL)
365 , distill_implicit_with_implicit_time_limitM(200LL)
366
367 //Gates
368 , doGateFind (false)
369 , maxGateBasedClReduceSize(20)
370 , doShortenWithOrGates(true)
371 , doRemClWithAndGates(true)
372 , doFindEqLitsWithGates(true)
373 , gatefinder_time_limitM(200)
374 , shorten_with_gates_time_limitM(200)
375 , remove_cl_with_gates_time_limitM(100)
376
377 //Gauss
378 , doM4RI(true)
379 , xor_detach_reattach(false)
380 , force_use_all_matrixes(false)
381
382 //Sampling
383 , sampling_vars(NULL)
384
385 //Timeouts
386 , orig_global_timeout_multiplier(3.0)
387 , global_timeout_multiplier(1.0) // WILL BE UNSET, NOT RELEVANT
388 , global_timeout_multiplier_multiplier(1.1)
389 , global_multiplier_multiplier_max(3)
390 , var_and_mem_out_mult(1.0)
391
392 //Multi-thread, MPI
393 , sync_every_confl(20000)
394 , thread_num(0)
395
396 //misc
397 , origSeed(0)
398 , reconfigure_val(0)
399 , reconfigure_at(2)
400 , preprocess(0)
401 , simulate_drat(false)
402 , saved_state_file("savedstate.dat")
403 {
404 ratio_keep_clauses[clean_to_int(ClauseClean::glue)] = 0;
405 ratio_keep_clauses[clean_to_int(ClauseClean::activity)] = 0.44;
406 }
407
408
print_times(const double time_used,const bool time_out,const double time_remain) const409 DLL_PUBLIC std::string SolverConf::print_times(
410 const double time_used
411 , const bool time_out
412 , const double time_remain
413 ) const {
414 if (do_print_times) {
415 std::stringstream ss;
416 ss
417 << " T: " << std::setprecision(2) << std::fixed << time_used
418 << " T-out: " << (time_out ? "Y" : "N")
419 << " T-r: " << time_remain*100.0 << "%";
420
421 return ss.str();
422 }
423
424 return std::string();
425 }
426
print_times(const double time_used,const bool time_out) const427 DLL_PUBLIC std::string SolverConf::print_times(
428 const double time_used
429 , const bool time_out
430 ) const {
431 if (do_print_times) {
432 std::stringstream ss;
433 ss
434 << " T: " << std::setprecision(2) << std::fixed << time_used
435 << " T-out: " << (time_out ? "Y" : "N");
436
437 return ss.str();
438 }
439
440 return std::string();
441 }
442
print_times(const double time_used) const443 DLL_PUBLIC std::string SolverConf::print_times(
444 const double time_used
445 ) const {
446 if (do_print_times) {
447 std::stringstream ss;
448 ss
449 << " T: " << std::setprecision(2) << std::fixed << time_used;
450
451 return ss.str();
452 }
453
454 return std::string();
455 }
456