Man page for GRASP This web page serves as an up to date man page for the GRASP SAT package. This man page is for the most recent version of GRASP. If you are using an older version, some of the options below may be unavailable. The ones not supported in the most recent version of GRASP are indicated. For running sat-grasp (for nsat is the same), issue the command: sat-grasp [options] < filename > Currently, you must specify a file name. The most often used options are the following: +Vn Set verbosity level to n. Higher n means more verbosity. +Bn Set the maximum number of backtracks to n. The default built-in value is 100,000. +Cn Set the maximum number of conflicts to n. The default built-in value is 200,000. +Sn Set the space growth to n * the original number of literals. The default built-in value for n is 100. +Tn Set the maximum CPU time to n seconds. The default built-in value for n is 10,000. +O Output the computed solution for satisfiable instances. +W Output the final CNF formula. +b[NCD] Type of backtracking performed. Only non-chronological backtracking implemented. Equivalent to +bN. +d< opt > Set variable selection heuristic to < opt >. See the source code for all the available options. Most often, < opt > is one of DLIS, MSMM, BOHM. +gn Allow for recorded clauses of size no greater than n to be added to CNF formula. If not specified, any recorded clause is added to the CNF formula. +rtn Set the relevance based learning to n, thus allowing clause to be deleted only after n literals become unassigned. +drN Randomize the chosen branching heuristic. N specifies the amount of randomness introduced. E.g.: N=1 randomizes the value selected; N=2 randomly breaks ties; N>=3 allows variables within (N-2)*10 percent of the largest heuristic figure being computed to randomly be selected. +drsN Use seed N when randomizing the branching heuristic. +wsN Largest size of recorded clauses to write when writing the final CNF formula (i.e. option +W selected). +sn Compute n solutions of the instance, provided n exist. +sa Compute all solutions of the instance. [+-]u Indentify (or not) UIPs. By default UIPs are identified. Other available options are the following: +iln Set the implication level to n. This defines the amount of learning allowed during the application of the deduction engine, i.e. the ability for identifying necessary assignments. +im[LGR] Implication mode used. Currently only +imR is implemented, allowing for recursive learning. +l Apply a (very) slow form of the pure literal rule. +pln Set the preprocessng level to n. This defines the amount of learning allowed during the application of the preprocessing engine, i.e. the ability for identifying necessary assignments. +pm[LGR] Preprocessing mode used. Currently only +pmR is implemented, allowing for recursive learning. +pb[ACLV]n Limit the number of considered assignments (A), clauses (C), literals (L) and variables (V) analyzed at each step of the recursive learning procedure. Any combination of options is allowed Other options, most still a prototype, are the following: +c Implement clause subsumtion among recorded clauses. This option is equivalent to +dc, and GRASP only recognizes +dc. +cj[AOC] Different forms of clause justification. NOT implemented. +dc Identify subsumption relations among clauses. +dv Identify subsumption relations among variables. Check the Binate Covering literature for more details on how this is actually done. +m Allow for multiple conflicts (i.e. unsatisfied clauses) to be identified and select the most promising one. This option is currently NOT implemented. +p Identify partitions of the CNF formula. Check the Binate Covering literature for more details on how this is actually done. This option is currently NOT implemented. +pr[FS] During preprocessing either find full (F) justifications or simple (S) justifications for identified necessary assignments. Simple justifications do not explain why a given necessary assignment was deemed necessary, so the resulting CNF formula is *not* equivalent to the original CNF formula, but it is satisfiable only if the original CNF was also satisfiable. +r Given a recorded clause, attempts to find a different set of literals that results in a smaller clause being recorded. This is done by expressing the recorded clause solely in terms of variables used for assignment selection purposes. [+-]sc Allows for the CNF formula to be declared satisfied even if some recorded clauses are not satisfied. By default all clauses must be satisfied. +t Removes redundant truth assignments from computed solutions. This can be useful if the goal is to compute solutions with a reduced number of specified assignments. This option is currently NOT implemented. _________________________________________________________________ Joao Marques Silva (E-mail: jpms@inesc.pt ) Last modified: Tue Nov 7 18:36:20 2000