Download User Manual - About ALCom

2
How to launch sKizzo
To launch sKizzo, use the following syntax.
sKizzo [OPTS] (FILE|DIR) [TIMEOUT]
where you have to provide:
1. An optional list of space-separated options OPTS. Such options are used to modify the
solving process and the input/output behavior of the solver. They are discussed in Section 3.
2. A mandatory DIR or FILE path:
(a) FILE, the full name (possibly with a path) of a DIMACS file containing the QBF
instance to be solved. The extension of this file has to be one of the following:
“.qdimacs”, “.dimacs”, “.qcnf”.
(b) DIR, the root of a directory subtree which is to be recursively visited. When you give
a directory as argument, the solver works in batch mode. See Section 4.
3. An optional TIMEOUT (in seconds). When a timeout is given, sKizzo works for no longer
than the specified amount of time, then gives up (exit code 30, see below).
Possible exit values for the command—returned to the program that called sKizzo or to the shell
from which the solver was launched—are:
10 on TRUE instances
20 on FALSE instances
30 on timeout
40 on a “unable to decide” condition
-1 on unrecoverable internal error
-2 on I/O error or file not found.
-3 on commandline parse error
-4 on DIMACS parse error
-5 on a SIGBUS/SIGSEV crash
-6 on unmanaged out-of-mem conditions
These return codes are valid when one single instance is given as argument. For the return codes
in batch mode see Section 4.2.
4