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