Controlling preprocessing and search time

In some situations preprocessing time exceeds the savings in time realized during search. In this case sbsat offers some ways to change the amount of preprocessing time performed. These include:

1. Change the preprocessing sequence to perform less iterations (see Section 5.1.2).
2. Specify a time limit, in seconds, for how long preprocessing can take. After the time limit has been reached the preprocessor will quit and sbsat will enter the search phase.
3. The user can terminate preprocessing interactively with ^C provided the switch -ctrl-c 1 is used on the command line.
4. The user can fast forward through preprocessing with the arrow key (a feature which is soon to be added).

An example of item 2 is the following:


$ sbsat small.cnf -max-preproc-time 180


which allows 3 minutes for preprocessing and continues to the search phase after that. This time constraint is checked between preprocessing options, so preprocessing could potentially terminate much later than desired.

Search time can also be controlled on the command line using a similar switch. For example,


$ sbsat small.cnf -max-branching-time 180


limits search time to 3 minutes.