1.5. Setting Parameters

CCalc can use several SAT solvers. By default, it calls mChaff and instructs it to stop as soon as one solution has been computed. Choices like these are determined by the values of parameters that can be changed by the user. The default values of these parameters are stored in the file options.std in the CCalc directory. To see their current values, type show_parameters: 
| ?- show_parameters.

    solver = mchaff
    solver_opts(mchaff) = ''
    num = 1
    file_io = true
    timed = true
    verbose = true
    compact = false
    optimize = true
    eliminate_tautologies = true
To see the list of solvers that can be called by CCalc, type help(solver): 
| ?- help(solver).

   The "solver" option establishes which satisfiability solver CCalc will
   call.  Valid values are:

   grasp      -- GRASP, Feb. 2000 version, by Joao Marques Silva
   mchaff     -- mChaff version spelt3, by Matthew Moskewicz
   relsat     -- relsat version 2.00, by Roberto Bayardo
   relsat_old -- relsat version 1.1.2, by Roberto Bayardo
   sato       -- SATO version 3.2, by Hantao Zhang
   sato_old   -- SATO version 3.1.2, by Hantao Zhang
   satz       -- Satz215.2, by Chu-Min Li
   satz-rand  -- satz-rand 4.9, by Henry Kautz
   walksat    -- WalkSAT version 41, by Henry Kautz and Bart Selman
   zchaff     -- zChaff, by Lintao Zhang
The values of parameters can be changed by the set command, for instance: 
| ?- set(solver,grasp).

yes
| ?- show_parameters.

    solver = grasp
    solver_opts = ''
    num = 1

| ?- set(num,all).

yes
| ?- show_parameters.

    solver = grasp
    solver_opts = ''
    num = all
By assigning value all to parameter num, the user instructs CCalc to find all answers to the query. If a positive integer n is assigned to num, CCalc will stop after generating n answers.

Another parameter you may find useful is dir. If you assign a value to it by typing

| ?- set(dir,path_name).

then CCalc will loadf files from the directory specified by path_name, instead of the directory from which you started CCalc.

Command reset_parameters restores all parameters to their default values.

Instead of changing the values of parameters by the set command, you can copy the options.std file to the directory from which you intend to start CCalc and modify that copy.

Exercise 1.5. Consider transition system TS1. How many edges ending at the vertex p=t are there in this graph? Instruct CCalc to calculate this number on the basis of the CCalc description of this transition system given in Section 1.1.

Exercise 1.6. How can we tell CCalc to find all vertices and all edges of a given transition system? Do this for the CCalc description of TS2 shown at the end of Section 1.1 for N=3.

Forward to Section 2.1: Basic Formulation
Back to Section 1.4: How CCalc Does It
Up to the Table of Contents