-
Notifications
You must be signed in to change notification settings - Fork 11
/
samd.c
73 lines (55 loc) · 2.28 KB
/
samd.c
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
65
66
67
68
69
70
/*
## ## ##### ##### $$$$$ $$$$ $$$$$$
## ## ## ## ## $$ $$ $$ $$
## ## ##### ## $$$$ $$$$$$ $$
## ## ## ## ## $$ $$ $$ $$
#### ##### ##### $$$$$ $$ $$ $$
======================================================
SLS SAT Solver from The University of British Columbia
======================================================
...Developed by Dave Tompkins (davet [@] cs.ubc.ca)...
------------------------------------------------------
.......consult legal.txt for legal information........
......consult revisions.txt for revision history......
------------------------------------------------------
... project website: http://www.satlib.org/ubcsat ....
------------------------------------------------------
.....e-mail ubcsat-help [@] cs.ubc.ca for support.....
------------------------------------------------------
*/
#include "ubcsat.h"
void SAMDUpdateVarLastChange();
void SAMDUpdateVarLastChangeW();
void AddSAMD() {
ALGORITHM *pCurAlg;
pCurAlg = CreateAlgorithm("samd","",FALSE,
"SAMD: Steepest Ascent Mildest Descent",
"Hansen and Jaumard [Computing 1990]",
"PickGSatTabu,SAMDUpdateVarLastChange",
"DefaultProcedures,Flip+VarScore",
"default","default");
CopyParameters(pCurAlg,"gsat-tabu","",FALSE);
CreateTrigger("SAMDUpdateVarLastChange",UpdateStateInfo,SAMDUpdateVarLastChange,"VarLastChange","UpdateVarLastChange");
pCurAlg = CreateAlgorithm("samd","",TRUE,
"SAMD: Steepest Ascent Mildest Descent (weighted)",
"Hansen and Jaumard [Computing 1990]",
"PickGSatTabuW,SAMDUpdateVarLastChangeW",
"DefaultProceduresW,Flip+VarScoreW",
"default_w","default");
CopyParameters(pCurAlg,"gsat-tabu","",1);
CreateTrigger("SAMDUpdateVarLastChangeW",UpdateStateInfo,SAMDUpdateVarLastChangeW,"VarLastChange","UpdateVarLastChange");
}
/* SAMD is essentially the same as GSAT-TABU,
except the age of flipped variables are not changed (and hence not tabu)
if they were flipped in an improving search step
*/
void SAMDUpdateVarLastChange() {
if (iBestScore >= 0) {
UpdateVarLastChange();
}
}
void SAMDUpdateVarLastChangeW() {
if (fBestScore >= FLOATZERO) {
UpdateVarLastChange();
}
}