kissat - Man Page

manual page for kissat sc2021


usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]

where '<option>' is one of the following common options:


print this list of all command line options


print only reduced list of command line options


force writing proofs (to existing CNF alike file)


do not print satisfying assignment


suppress all messages (see also '--quiet')


print all statistics (see also '--statistics')


increase verbose level (see also '--verbose')

Further '<option>' can be one of the following less frequent options:


print solver information


print build information


use colors (default if connected to terminal)


no colors (default if not connected to terminal)


print compiler information


print copyright information


same as '-f' (force writing proof)


print 'git' identifier (SHA-1 hash)


print option range list


relaxed parsing (ignore DIMACS header)


stricter parsing (no empty header lines)


print version

The following solving limits can be enforced:




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 CDCL solving ('--plain' but no restarts, minimize, reduce)


default configuration


plain CDCL solving without advanced techniques


target satisfiable instances ('--target=2 --restartint=50')


target unsatisfiable instances ('--stable=0')

Or '<option>' is one of the following long options:


extract and eliminate and gates [true]


enable autarky reasoning [true]


delay autarky reasoning [false]


binary clause backbone (2=eager) [1]


delay backbone computation [false]


relative effort in per mille [20]


focus on not-yet-tried literals [false]


keep backbone candidates [true]


maximum backbone rounds [1e3]


backbone rounds limit [100]


backward subsumption in BVE [true]


bump reason side literals too [true]


relative reason literals limit [10]


decision rate limit [10]


sample cached assignments [true]


allow chronological backtracking [true]


maximum jumped over levels [100]


enable compacting garbage collection [true]


compact inactive limit (in percent) [10]


per mille scores decay [50]


how many cores [2]


extract general definitions [true]


usable defragmentation limit in percent [75]


size defragmentation limit [2^18]


maximum delay (autarky, failed, ...) [2]


eagerly subsume recently learned clauses [20]


bounded variable elimination (BVE) [true]


maximum elimination bound [16]


elimination clause size limit [100]


delay variable elimination [false]


relative effort in per mille [100]


use heap to schedule elimination [false]


initial elimination interval [500]


base elimination interval [500]


keep elimination candidates [true]


elimination occurrence limit [1e3]


elimination rounds limit [2]


fast exponential moving average window [33]


slow exponential moving average window [1e5]


extract and eliminate equivalence gates [true]


extract gates in variable elimination [true]


failed literal probing [true]


continue if many failed (in percent) [90]


delay failed literal probing [true]


minimum probe effort [50]


failed literal probing rounds [2]


force initial phase [false]


forward subsumption in BVE [true]


relative effort in per mille [100]


on-the-fly hyper binary resolution [true]


extract and eliminate if-then-else gates [true]


enable incremental solving [false]


minimum absolute effort [1e4]


learned clause minimization [true]


minimization depth [1e3]


count ticks in minimize and shrink [true]


initial focused conflicts limit [1e3]


initial focused ticks limit [1e8]


on-the-fly strengthening [true]


initial decision phase [true]


enable phase saving [true]


enable probing [true]


delay probing [false]


initial probing interval [100]


probing interval [100]


profile level [2]


promote clauses [true]


disable all messages [false]


delay preprocessing after scheduling [true]


enable radix-heap for shrinking [false]


learned clause reduction [true]


reduce fraction in percent [75]


initial reduce interval [300]


base reduce interval [1e3]


restart at reduce (1=stable,2=always) [0]


stable reluctant doubling restarting [true]


reluctant interval [2^10]


reluctant limit (0=unlimited) [2^20]


reinitialization of decision phases [true]


rephase best phase [true]


initial rephase interval [1e3]


base rephase interval [1e3]


rephase inverted phase [true]


rephase original phase [true]


initial 'OI' prefix repetition [1]


rephase walking phase [true]


enable restarts [true]


base restart interval [1]


fast/slow margin in percent [10]

--restartreusetrail=<bool> restarts reuse trail [true]


random seed [0]


learned clauses (1=bin,2=lrg,3=rec) [3]


minimize during shrinking [true]


enable probing and elimination [true]


enable stable search mode [1]


print complete statistics [false]


equivalent literal substitution [true]


maximum substitution round effort [10]


maximum substitution rounds [2]


subsumption clause size limit [1e3]


subsumption occurrence limit [1e3]


target phases (1=stable,2=focused) [1]


enable hyper ternary resolution [true]


delay hyper ternary resolution [true]


relative effort in per mille [70]


use heap to schedule ternary resolution [true]


maximum clauses added in percent [20]


learned clause tier one glue limit [2]


learned clause tier two glue limit [6]


transitive reduction of binary clauses [true]


relative effort in per mille [20]


keep transitivity candidates [true]


tumbled external indices order [true]


verbosity level [0]


vivify clauses [true]


relative effort in per mille [100]


remove implied redundant clauses [2]


relative irredundant effort [1]


keep vivification candidates [false]


relative tier1 effort [3]


relative tier2 effort [6]


relative effort in per mille [5]


fit CB value to average clause length [true]


initial local search [false]


reuse walking results (2=always) [1]


use clause weights [true]


extract and eliminate XOR gates [true]


minimum elimination bound [1]


XOR extraction clause size limit [5]

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.


July 2021 kissat sc2021