-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME.txt
139 lines (100 loc) · 4.99 KB
/
README.txt
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
Cachet 1.21 for Weighted Model Counting, July, 2005
Department of Computer Science and Engineering, University of Washington
COMPILATION:
In the source directory, typing
make
will create cachet.
USAGE:
cachet cnf_file [-t time_limit]
[-c cache_size]
[-o oldest_cache_entry]
[-l cache_clean_limit]
[-h heuristic_selection]
[-s static variable ordering on]
[-r cross-implication off]
[-b far-backtracking-factor]
[-f 2nd far-backtracking on]
[-a adjusting-component-ordering off]
[-n max_num_learned_clause]
[-q quiet]
OPTIONS:
-t time_limit: default 48 hours.
-c cache_size: set size of hash table; By default, 5M.
The hash table is implemented as separate chaining, so this size is
the largest number of distinct chains, not the number of hashed values
(controlled by the following two parameters).
IMPORTANT: larger value may decrease #collisions and thus time for
chain lookup but increase time for computing hash indexes and system
overhead.
-o oldest_cache_entry: perform lazy deletion of hash table entries
older than oldest_cache_entry whenever a chain is searched.
Default value is 1M.
IMPORTANT: this parameter may need to be adjusted up or down by the
user in order to maximize hash hits while avoiding exhausting
physical memory.
-l cache_clean_limit: perform a global cleanup, deleting 3/4 top old
entries, if the total length of all chains in the hash table exceeds
this number. Default value is 20 * oldest_cache_entry (set by -o).
Usually there is no need to adjust this parameter.
-h heuristic_selection: select one of the eight branch heuristics,
default value is -h 5.
-h 0: select var by largest degree, tie-break lexigraphically
-h 1: select var by largest degree, tie-break by sum of degrees
-h 2: select var by sum of degrees, tie-break, chronologically
-h 3: select var by sum of degrees, tie-break by largest degree(DLCS)
-h 4: Variable State Independent Decaying Sum (VSIDS)
-h 5: Variable State Aware Decaying Sum (VSADS, default)
-h 6: Exact Unit Propagation Count (EUPC)
-h 7: Approximate Unit Propagation Count (AUPC)
-s static_var_ordering_file: use static+dynamic heuristic with
static ordering specified by the file and dynamic heuristic
specified by -h option.
IMPORTANT: in particular, static_var_ordering_file can be generated by
dtree-based static variable ordering method, code from Jinbo Huang and
Adnan Darwiche, UCLA.
There is an executable file called "preprocess_cnf" that generates
dtree-based static_var_ordering_file.
-r : turn off default cross-component implications.
-a : turn off defualt smallest component selection.
-b far-backtracking-factor: specify a factor in [0,2], where 0 means
complete far-backtracking on and 2 means off (2 by default)
-f : turn on 2nd far-backtracking scheme other than -b 0 (off by default)
-q quiet: only output #solutions, no other summary information.
EXAMPLES:
cachet prob004-log-a.pddl.cnf
(Using all default parameters)
cachet prob004-log-a.pddl.cnf -h 6
(selecting heuristic 6(EUPC))
cachet prob004-log-a.pddl.cnf -h 7 -s static_ordering.txt
(Using static-ordering in static_ordering.txt + heuristic 7(AUPC).
static_ordering.txt can be obtained by running preprocess_cnf, for example:
preprocess_cnf prob004-log-a.pddl.cnf static_ordering.txt
or specified by user following the same format)
cachet prob005-log-b.pddl.cnf -t 3600 -c 10000000 -o 2000000 -b 0 -r -a -h 3
(Setting time-limit 3600 seconds, cache_size 10000000,
largest-age-entry in a chain 2000000, complete far-backtracking on,
turning off cross-component-implications, turning off adjusting
component ordering for branching, selecting heuristic 3(DLCS))
COMMENTS:
-o must be set appropriately for hard problems.
-l should be much larger (e.g. 20*) than the value set by -o.
-c: larger_cache_size decreases the number of cache collisions, but increases
the time for computing hash indexes and results less on-chain deletion.
-h: the performance of different heuristics can be quite different.
-s: static-ordering + dynamic heuristic works better for some problems.
Dtree method often generates good static ordering, or if user has some
knowledge about which variables should be set first, it is good to
indicate them in this way. In the static var ordering file, vars appearing
earlier have higher priorities to be set in search, and different priority
groups are seperatd by 0. Different vars in the same group are chosen by
dynamic heuristic specified by -h option.
-r -a: for better performance, usually should not be turned off.
-n 0 turns off clause learning.
-c 1 -o 1 turns off caching.
WEIGHTS IN CNF
A normal variable weight is in [0,1], specified by line starting with 'w'
var index, and weight. It is assumed weight(x)+weight(-x)=1,
except weight -1 which means weight(x)=weight(-x)=1, corresponding to an
internal node in Bayesian Networks. By default, every variable weight
is set to 0.5, if its value not given in CNF.
TODO before compilation ln -s /usr/src/linux-headers-3.2.0-25/include/linux/sys.h /usr/include/linux/sys.h