| Prover9 Manual |
| Version 2009-11A |
assign(sos_limit, n). % default n=20000, range [-1 .. INT_MAX]
This parameter imposes a limit on the size of the sos list (n=-1 means there is no limit). It also activates a method for deleting clauses (in addition to, and after, application of the max_weight parameter).This is a little bit tricky (and sometimes too clever for its own good). When the sos is half full, it starts being selective about keeping clauses, and as it fills up, it gradually becomes more selective. When it is full, it is very selective about keeping clauses. (The method is not applied to clauses that match hints.) When it decides to keep a clause, and the sos is already full, the "worst" clause in sos is deleted to make room for the new clause.
More details will be added later.
assign(max_given, n). % default n=-1, range [-1 .. INT_MAX]
This parameter will stop the search after n given clauses have been used. A value of -1 means that there is no limit.
assign(max_kept, n). % default n=-1, range [-1 .. INT_MAX]
The search will stop when more than n clauses have been retained.
assign(max_megs, n). % default n=200, range [-1 .. INT_MAX]
The search will stop when about n megabytes of memory have been used.
assign(max_seconds, n). % default n=-1, range [-1 .. INT_MAX]
The search will stop at about n seconds. For UNIX-like systems, the "user CPU" time is used.
assign(max_minutes, n). % default n=-1, range [-1 .. INT_MAX]
Changing this parameter simply changes max_seconds to the corresponding value.
assign(max_hours, n). % default n=-1, range [-1 .. INT_MAX]
Changing this parameter simply changes max_seconds to the corresponding value.
assign(max_days, n). % default n=-1, range [-1 .. INT_MAX]
Changing this parameter simply changes max_seconds to the corresponding value.