Prover9 Manual |  | Version 2009-02A

# Search Limits

    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.

Next Section: The Loop