LS-solver/settings.h at master · OlhaHn/LS-solver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
#ifndef SETTINGS_H
#define SETTINGS_H

#endif //SETTINGS_H

#ifndef DIFF_HEURISTIC
#define DIFF_HEURISTIC 3

/*
    Possible values:
        0 "crh" - clause reduction heuristic,
        1 "wbh" - weighted binaries heuristic,
        2 "bsh" - backbone search heuristic,
        3 "bsrh" - backbone search renormalized heuristic
*/

#endif // DIFF_HEURISTIC

#ifndef DECISION_HEURISTIC
#define DECISION_HEURISTIC 1

/*
    Possible values:
        0 "kcnfs" - selects 1 if x appears more often then -x,
        1 "march" - selects 1 if diff(x=1) < diff(x=2)
        2 "posit" - selects 0 if x appears more often then -x,
        3 "satz" - always select 1 first
*/
#endif // DECISION_HEURISTIC

#ifndef PRESELECT_HEURISTIC
#define PRESELECT_HEURISTIC 0

/*
    Possible values:
        0 propz
        1 clause reduction approximation
*/
#endif // PRESELECT_HEURISTIC

#ifndef AUTARKY_REASONING
#define AUTARKY_REASONING 1

/*
    Possible values:
        0 don't use autarky_reasoning
        1 use autarky_reasoning
*/

#endif


#ifndef DOUBLE_LOOKAHEAD
#define DOUBLE_LOOKAHEAD 1
/*
    possible values:
        0 don't use double lookahead
        1 use double look ahead with trigger = 65
        2 use double look ahead with trigger = 0.17 * n
        3 use dynamic look ahead with trigger on start 0.17*n, reduced after each unsuccessfull double look-ahead
        4 use dynamic look ahead with trigger on start 0, updated after each unsuccessfull double look-ahead, reduced slightly after each look-ahead
*/

#endif