SettingsNuts And Bolts

The SETTINGS button allows you to change some of the parameters controlling the solver’s behaviour. There is an option button allowing you to change formula mode, three more with which you can set certain numerical values, and three with which you can choose verbosity settings. Briefly:

FOF form / Clause form
This toggle allows you to switch between the two modes of formula input. FOF (First Order Formula) form is closer to the notation usually found in logic textbooks, while clause form is closer to the version of logic used by most automated reasoning systems.

Number of solutions
By default, up to three solutions are printed before the search is “stopped by the limit on the number of solutions”. It may happen, for some problems, that you know there are many solutions but you only want one of them. In that case, you can set the limit to one. At the other extreme, it is also possible to print all solutions, however many there may be. Be careful with this option, as the resulting output may be very long in some cases.

Time in seconds
This button lets you set a time limit. A few puzzles, especially from the “logician” list, may be hard enough to make the solver work for more than a second, so you may give it a more generous limit if you wish. It is a bad idea to over-use this option. For almost all of the puzzles, you don’t need it. In any case there is no free lunch: the higher you set the time limit, the lower the priority given to your solver run, so you do not automatically gain from raising the time limit unless there happen to be few other users on the machine.

Pretest limit
This controls the cutoff weight above which clauses are evaluated lazily (i.e. they are not turned into constraints until some potential model violates them). This is really technical stuff which you are hardly likely to need to touch. If the solver is timing out on you, it may be worth trying an increase in the pretest limit, just to see what happens.

Printing the job
If you ask for the job to be printed, you will see the input actually sent to the solver. You probably don’t want to, though it can be of some use for diagnosing certain errors such as mis-spelt names or parentheses in the wrong place. Note that the formulae are shown after conversion to clause form, so it may not be trivial to relate them back to the ones you wrote.

Printing the solutions
It is just possible that, for instance, you wish to turn off printing of the solutions so as just to count them without producing lengthy output. The setting “none” does that. The setting “brief” causes printing of each solution to start with the first function that is different from what it was in the previous solution. “Full” is the default.

Printing statistics
You may also wish to see detailed stats on the search, including the number of low-level constraints generated and some information on the branching behaviour of the algorithm. The number of backtracks or number of values inserted may be of interest for purposes of comparison between encodings of a problem, as they are measures of the amount of work done. The exact description of all the stats reported is beyond the scope of these notes.