1		:- module(cdclt_settings, [restart_policy/1,
2		static_syntax_analysis/1,
3		static_smt_symmetry_breaking/1,
4		luby_restart_unit_length/1,
5		glucose_restart_recent_lbds_threshold/1,
6		glucose_restart_margin_ratio/1,
7		glucose_restart_trail_threshold/1,
8		glucose_restart_stack_avg_factor/1,
9		discard_clause_greater_lbd/1,
10		discard_learned_clauses_frequency_constant/1,
11		discard_learned_clauses_constant_factor/1,
12		decision_heuristic/1,
13		bump_scores_for_bj_clause_only/1,
14		glue_bumping/1,
15		vsids_decay_value/1,
16		vsids_decay_frequency/1,
17		evsids_f_value/1,
18		clause_learning/1,
19		print_logs/1,
20		log_stats/1,
21		clause_minimization/1,
22		minimize_theory_explanations/1,
23		binary_boost_factor/1,
24		sat_var_assignment_timeout/1,
25		preprocessing/1]).
26
27		:- use_module(probsrc(preferences), [get_preference/2]).
28		:- use_module(probsrc(module_information), [module_info/2]).
29
30		:- module_info(group, cdclt).
31		:- module_info(description,'This module provides settings for the CDCL(T) solver.').
32
33		log_stats(false).
34		print_logs(false).
35
36		% Remove clauses that are subsumed by another clause. For instance, (A or B) subsumes (A or B or C).
37		preprocessing(subsuming).
38		% Apply Boolean resolution once and replace clauses that are subsumed by the resolvent.
39		%preprocessing(resolution_subsuming).
40
41		clause_learning(true).
42		static_syntax_analysis(X) :-
43		get_preference(cdclt_perform_static_analysis, X).
44		static_smt_symmetry_breaking(X) :-
45		get_preference(cdclt_perform_symmetry_breaking, X).
46
47		% time limit for assigning a SAT variable in ProB's deterministic propagation phase before grounding
48		sat_var_assignment_timeout(10000).
49
50		% minimize theory explanations by computing an unsatisfiable core
51		minimize_theory_explanations(true).
52
53		% factor for boosting heuristic scores of variables that occur in binary clauses
54		binary_boost_factor(1). % factor 1 means no boosting
55
56		%% Random Restarts
57		% Available restart policies: luby, glucose.
58		restart_policy(glucose).
59		% The length of a unit in the Luby sequence.
60		luby_restart_unit_length(32).
61		% The amount of conflict clauses to be considered "recent" in Glucose restarts. Small value leads to more restarts.
62		glucose_restart_recent_lbds_threshold(200).
63		% Do restart if defined proportion of recent LBDs average is greater than total average. Large value leads to more restarts.
64		glucose_restart_margin_ratio(0.8).
65		% The amount of conflicts to enable possible emptying of the recent LBD queue to favor SAT instances too.
66		glucose_restart_trail_threshold(5000).
67		% For factor f, the last stack size needs to be larger than f * recentSizes.avg() to empty the recent LBD queue.
68		glucose_restart_stack_avg_factor(1.4).
69		%%
70
71		%% Reducing Learned Clauses
72		% Maximum LBD score for learned clauses.
73		% Each learned clause is propagated at least once independent of its actual LBD score.
74		discard_clause_greater_lbd(5).
75		% Remove half of the learned clauses every "frequency_constant + constant_factor * x" conflicts, where x is the amount of reductions so far.
76		discard_learned_clauses_frequency_constant(20000).
77		discard_learned_clauses_constant_factor(500).
78		%%
79
80		% local: Generate the 1-UIP clause. Mark all its literals. Remove those implied variables which have all their antecedent literals marked.
81		% recursive: Generate the 1-UIP clause. Mark its literals. Implied variables in 1-UIP clause are candidates for removal. Search implication graph. Start from antecedent literals of candidate. Stop at marked literals or decisions. If search always ends at marked literals then the candidate can be removed.
82		% none for no minimization
83		clause_minimization(local).
84
85		%% Decision Heuristic
86		% Available decision heuristics: vsids, evsids, acids, vmtf.
87		decision_heuristic(acids).
88		bump_scores_for_bj_clause_only(false).
89		% Additionally bump glue variables (see https://www.cs.cmu.edu/~mdsolimc/phd_thesis.pdf).
90		glue_bumping(false).
91		% Decision score s is updated by s/v.
92		vsids_decay_value(2).
93		% Amount of found conflicts when to decay scores.
94		vsids_decay_frequency(128).
95		% A value between 0 and 1. Decision score s is updated by s + f^(-k).
96		evsids_f_value(0.95).
97		%%