Prover9 Manual Version June-2006

Search Limits

assign(sos_limit, n).  % default n=10000, 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. 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.