kissat - Man Page
manual page for kissat 3.1.1
Description
usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]
where '<option>' is one of the following common options:
- --help
print this list of all command line options
- -h
print only reduced list of command line options
- -f
force writing proofs (to existing CNF alike file)
- -n
do not print satisfying assignment
- -q
suppress all messages (see also '--quiet')
- -s
print all statistics (see also '--statistics')
- -v
increase verbose level (see also '--verbose')
Further '<option>' can be one of the following less frequent options:
- --banner
print solver information
- --build
print build information
- --color
use colors (default if connected to terminal)
- --no-color
no colors (default if not connected to terminal)
- --compiler
print compiler information
- --copyright
print copyright information
- --force
same as '-f' (force writing proof)
- --id
print 'git' identifier (SHA-1 hash)
- --range
print option range list
- --relaxed
relaxed parsing (ignore DIMACS header)
- --strict
stricter parsing (no empty header lines)
- --version
print version
The following solving limits can be enforced:
--conflicts=<limit>
--decisions=<limit>
--time=<seconds>
Satisfying assignments have by default values for all variables unless '--partial' is specified, then only values are printed for variables which are necessary to satisfy the formula.
The following predefined 'configurations' (option settings) are supported:
- --basic
basic CDCL solving ('--plain' but no restarts, minimize, reduce)
- --default
default configuration
- --plain
plain CDCL solving without advanced techniques
- --sat
target satisfiable instances ('--target=2 --restartint=50')
- --unsat
target unsatisfiable instances ('--stable=0')
Or '<option>' is one of the following long options:
- --ands=<bool>
extract and eliminate and gates [true]
- --backbone=0..2
binary clause backbone (2=eager) [1]
- --backboneeffort=0..1e5
effort in per mille [20]
- --backbonemaxrounds=1...
maximum backbone rounds [1e3]
- --backbonerounds=1...
backbone rounds limit [100]
- --bump=<bool>
enable variable bumping [true]
- --bumpreasons=<bool>
bump reason side literals too [true]
- --bumpreasonslimit=1...
relative reason literals limit [10]
- --bumpreasonsrate=1...
decision rate limit [10]
- --chrono=<bool>
allow chronological backtracking [true]
- --chronolevels=0...
maximum jumped over levels [100]
- --compact=<bool>
enable compacting garbage collection [true]
- --compactlim=0..100
compact inactive limit (in percent) [10]
- --decay=1..200
per mille scores decay [50]
- --definitioncores=1..100
how many cores [2]
- --definitions=<bool>
extract general definitions [true]
- --definitionticks=0...
kitten ticks limits [1e6]
- --defraglim=50..100
usable defragmentation limit in percent [75]
- --defragsize=10...
size defragmentation limit [2^18]
- --eliminate=<bool>
bounded variable elimination (BVE) [true]
- --eliminatebound=0..2^13
maximum elimination bound [16]
- --eliminateclslim=1...
elimination clause size limit [100]
- --eliminateeffort=0..2e3
effort in per mille [100]
- --eliminateinit=0...
initial elimination interval [500]
- --eliminateint=10...
base elimination interval [500]
- --eliminateocclim=0...
elimination occurrence limit [2e3]
- --eliminaterounds=1..1e4
elimination rounds limit [2]
- --emafast=10..1e6
fast exponential moving average window [33]
- --emaslow=100..1e6
slow exponential moving average window [1e5]
- --equivalences=<bool>
extract and eliminate equivalence gates [true]
- --extract=<bool>
extract gates in variable elimination [true]
- --flushproof=<bool>
flush proof lines immediately [false]
- --forcephase=<bool>
force initial phase [false]
- --forward=<bool>
forward subsumption in BVE [true]
- --forwardeffort=0..1e6
effort in per mille [100]
- --ifthenelse=<bool>
extract and eliminate if-then-else gates [true]
- --incremental=<bool>
enable incremental solving [false]
- --mineffort=0...
minimum absolute effort in millions [10]
- --minimize=<bool>
learned clause minimization [true]
- --minimizedepth=1..1e6
minimization depth [1e3]
- --minimizeticks=<bool>
count ticks in minimize and shrink [true]
- --modeinit=10..1e8
initial focused conflicts limit [1e3]
- --modeint=10..1e8
focused conflicts interval [1e3]
- --otfs=<bool>
on-the-fly strengthening [true]
- --phase=<bool>
initial decision phase [true]
- --phasesaving=<bool>
enable phase saving [true]
- --probe=<bool>
enable probing [true]
- --probeinit=0...
initial probing interval [100]
- --probeint=2...
probing interval [100]
- --profile=0..4
profile level [2]
- --promote=<bool>
promote clauses [true]
- --quiet=<bool>
disable all messages [false]
- --randec=<bool>
random decisions [true]
- --randecfocused=<bool>
random decisions in focused mode [true]
- --randecinit=0...
random decisions interval [500]
- --randecint=0...
initial random decisions interval [500]
- --randeclength=1...
random conflicts length [10]
- --randecstable=<bool>
random decisions in stable mode [false]
- --reduce=<bool>
learned clause reduction [true]
- --reducefraction=10..100
reduce fraction in percent [75]
- --reduceinit=2..1e5
initial reduce interval [1e3]
- --reduceint=2..1e5
base reduce interval [1e3]
- --reluctant=<bool>
stable reluctant doubling restarting [true]
- --reluctantint=2..2^15
reluctant interval [2^10]
- --reluctantlim=0..2^30
reluctant limit (0=unlimited) [2^20]
- --rephase=<bool>
reinitialization of decision phases [true]
- --rephaseinit=10..1e5
initial rephase interval [1e3]
- --rephaseint=10..1e5
base rephase interval [1e3]
- --restart=<bool>
enable restarts [true]
- --restartint=1..1e4
base restart interval [1]
- --restartmargin=0..25
fast/slow margin in percent [10]
- --seed=0...
random seed [0]
- --shrink=0..3
learned clauses (1=bin,2=lrg,3=rec) [3]
- --simplify=<bool>
enable probing and elimination [true]
- --stable=0..2
enable stable search mode [1]
- --statistics=<bool>
print complete statistics [false]
- --substitute=<bool>
equivalent literal substitution [true]
- --substituteeffort=1..1e3
effort in per mille [10]
- --substituterounds=1..100
maximum substitution rounds [2]
- --subsumeclslim=1...
subsumption clause size limit [1e3]
- --subsumeocclim=0...
subsumption occurrence limit [1e3]
- --sweep=<bool>
enable SAT sweeping [true]
- --sweepclauses=0...
environment clauses [2^10]
- --sweepdepth=0...
environment depth [2]
- --sweepeffort=0..1e4
effort in per mille [100]
- --sweepfliprounds=0...
flipping rounds [1]
- --sweepmaxclauses=2...
maximum environment clauses [2^15]
- --sweepmaxdepth=1...
maximum environment depth [3]
- --sweepmaxvars=2...
maximum environment variables [2^13]
- --sweepvars=0...
environment variables [2^8]
- --target=0..2
target phases (1=stable,2=focused) [1]
- --tier1=1..100
learned clause tier one glue limit [2]
- --tier2=1..1e3
learned clause tier two glue limit [6]
- --transitive=<bool>
transitive reduction of binary clauses [true]
- --transitiveeffort=0..2e3
effort in per mille [20]
- --transitivekeep=<bool>
keep transitivity candidates [true]
- --tumble=<bool>
tumbled external indices order [true]
- --verbose=0..3
verbosity level [0]
- --vivify=<bool>
vivify clauses [true]
- --vivifyeffort=0..1e3
effort in per mille [100]
- --vivifyirr=1..100
relative tier1 effort [1]
- --vivifytier1=1..100
relative tier1 effort [1]
- --vivifytier2=1..100
relative tier2 effort [1]
- --walkeffort=0..1e6
effort in per mille [50]
- --walkinitially=<bool>
initial local search [false]
- --warmup=<bool>
initialize phases by unit propagation [true]
Furthermore '<dimacs>' is the input file in DIMACS format. The solver reads from '<stdin>' if '<dimacs>' is unspecified. If the path has a '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix then the solver tries to find a corresponding decompression tool ('bzip2', 'gzip', 'lzma', '7z', or 'xz') to decompress the input file on-the-fly after checking that the input file has the correct format (starts with the corresponding signature bytes).
If '<proof>' is specified then a proof trace is written to the given file. If the file name is '-' then the proof is written to '<stdout>'. In this case the ASCII version of the DRAT format is used. For real files the binary proof format is used unless '--no-binary' is specified.
Writing of compressed proof files follows the same principle as reading compressed files. The compression format is based on the file suffix and it is checked that the corresponding compression utility can be found.