1		:- module(dpllt_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		vsids_decay_value/1,
15		vsids_decay_frequency/1,
16		evsids_f_value/1]).
17
18		:- use_module(probsrc(preferences), [get_preference/2]).
19		:- use_module(probsrc(module_information), [module_info/2]).
20
21		:- module_info(group, dpllt).
22		:- module_info(description,'This module provides settings for the DPLL(T) solver.').
23
24		%:- dynamic static_smt_symmetry_breaking/1, static_syntax_analysis/1.
25
26		static_syntax_analysis(X) :- get_preference(dpllt_perform_static_analysis,X).
27		static_smt_symmetry_breaking(X) :- get_preference(dpllt_perform_symmetry_breaking,X).
28		%% Random Restarts
29		% Available restart policies: luby, glucose.
30		restart_policy(glucose).
31		% The length of a unit in the Luby sequence.
32		luby_restart_unit_length(32).
33		% The amount of conflict clauses to be considered "recent" in Glucose restarts. Small value leads to more restarts.
34		glucose_restart_recent_lbds_threshold(50).
35		% Do restart if defined proportion of recent LBDs average is greater than total average. Large value leads to less restarts.
36		glucose_restart_margin_ratio(0.8).
37		% The amount of conflicts to enable possible emptying of the recent LBD queue to favor SAT instances too.
38		glucose_restart_trail_threshold(5000).
39		% For factor f, the last stack size needs to be larger than f * recentSizes.avg() to empty the recent LBD queue.
40		glucose_restart_stack_avg_factor(1.4).
41		%%
42
43		%% Reducing Learned Clauses
44		% Maximum LBD score for learned clauses.
45		% Each learned clause is propagated at least once independent of its actual LBD score.
46		discard_clause_greater_lbd(5).
47		% Remove half of the learned clauses every "frequency_constant + constant_factor * x" conflicts.
48		discard_learned_clauses_frequency_constant(20000).
49		discard_learned_clauses_constant_factor(500).
50		%%
51
52		%% Decision Heuristic
53		% Available decision heuristics: vsids, evsids.
54		decision_heuristic(evsids).
55		bump_scores_for_bj_clause_only(true).
56		% Decision score s is updated by s/v.
57		vsids_decay_value(2).
58		% Amount of found conflicts when to decay scores.
59		vsids_decay_frequency(128).
60		% A value between 0 and 1. Decision score is updated by s + f^(-k).
61		evsids_f_value(0.9).
62		%%