Download User Manual - About ALCom

Contents
1
Introduction
1.1 Contact and feedback . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
3
2
How to launch sKizzo
4
3
Command-line options
3.1 Options that modify the personality of the solver . . . . . .
3.2 Options to tune the Q style (qbf reasoning) . . . . . . . . .
3.3 Options to tune the S style (incomplete symbolic reasoning)
3.4 Options to tune the R style (complete symbolic reasoning) .
3.5 Options to tune the B style (branching reasoning) . . . . . .
3.6 Options to tune the G style (SAT-based reasoning) . . . . . .
3.7 Options to control memory usage . . . . . . . . . . . . . . .
3.8 Options to make sKizzo stop on certain occurrences . . . . .
3.9 Options to control verbosity, dumping, logging . . . . . . .
3.10 Miscellaneous options . . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5
5
6
7
10
10
10
11
12
12
13
Batch mode
4.1 Order of processing . . . . . . . . .
4.2 Return values . . . . . . . . . . . .
4.3 Timeouts . . . . . . . . . . . . . .
4.4 Interaction among solution processes
4.5 Commandline parameters . . . . . .
4.6 Reporting . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
14
14
14
14
15
15
16
Notes on run-time behavior, memory consumption, solving personalities
5.1 Tuning your solving personality . . . . . . . . . . . . . . . . . . . .
5.2 Memory consumption . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3 Shell commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4 Multiprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18
18
18
19
19
4
5
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
6 sKizzo’s internals
20
6.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
6.2 Problem Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
6.3 Inference Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
References
23
Appendix A: Copyright and License
24
2