Scroll to navigation

KISSAT(1) User Commands KISSAT(1)

NAME

kissat - Kissat Satisfiability Solver

DESCRIPTION

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)
print logging messages (see also '--log')
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
print embedded option list
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:

--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 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]
binary clause backbone (2=eager) [1]
effort in per mille [20]
maximum backbone rounds [1e3]
backbone rounds limit [100]
big binary clause fraction per mille [990]
enable variable bumping [true]
bump reason side literals too [true]
relative reason literals limit [10]
decision rate limit [10]
check model (1) and derived clauses (2) [2]
allow chronological backtracking [true]
maximum jumped over levels [100]
enable compacting garbage collection [true]
compact inactive limit (in percent) [10]
congruence closure on extracted gates [true]

--congruenceandarity=2..5e7 AND gate arity limit [1e6]

extract AND gates for congruence closure [true]

--congruencebinaries=<bool> extract certain binary clauses [true]

extract ITE gates for congruence closure [true]
congruence closure only initially [false]

--congruencexorarity=2..20 congruence XOR gate arity limit [4]

--congruencexorcounts=1... XOR counting rounds [2]

extract XOR gates for congruence closure [true]
per mille scores decay [50]
how many cores [2]
extract general definitions [true]
kitten ticks limits [1e6]
usable defragmentation limit in percent [75]
size defragmentation limit [2^18]
eagerly subsume previous learned clauses [4]
bounded variable elimination BVE [true]
maximum elimination bound [16]
elimination clause size limit [100]
effort in per mille [100]
initial elimination interval [500]
base elimination interval [500]
elimination occurrence limit [2e3]
elimination rounds limit [2]
fast exponential moving average window [33]
slow exponential moving average window [1e5]
parse and apply embedded options [true]
extract and eliminate equivalence gates [true]
extract gates in variable elimination [true]
bounded variable addition [true]
candidates reduction rounds [2]
bounded variable effort in per mille [50]
structural factoring heuristic hops [3]
initial ticks ticks in millions [700]
bounded variable addition clause size [5]
structural bounded variable addition [false]
initial fast variable elimination [true]
fast elimination clause length limit [100]
fast elimination resolvents limit [8]
fast elimination occurrence limit [100]
fast elimination rounds [4]
forward subsuming fast variable elimination [true]
flush proof lines immediately [false]
always used focused mode tiers [true]
force initial phase [false]
forward subsumption in BVE [true]
effort in per mille [100]
extract and eliminate if-then-else gates [true]
enable incremental solving [false]
jump binary reasons [true]
logging level (1=on,2=more,3=check,4/5=mem) [0]
try some lucky assignments [true]
lucky assignments before preprocessing [true]
lucky assignments after preprocessing [true]
minimum absolute effort in millions [10]
learned clause minimization [true]
minimization depth [1e3]
count ticks in minimize and shrink [true]
initial focused conflicts limit [1e3]
focused conflicts interval [1e3]
on-the-fly strengthening [true]
initial decision phase [true]
enable phase saving [true]
initial preprocessing [true]

--preprocessbackbone=<bool> backbone preprocessing [true]

--preprocesscongruence=<bool> congruence preprocessing [true]

variable addition preprocessing [true]
probing preprocessing [true]
initial preprocessing rounds [1]
sweep preprocessing [true]
enable probing [true]
initial probing interval [100]
probing interval [100]
probing rounds [2]
profile level [2]
promote clauses [true]
disable all messages [false]
random decisions [true]
random decisions in focused mode [true]
random decisions interval [500]
initial random decisions interval [500]
random conflicts length [10]
random decisions in stable mode [false]
learned clause reduction [true]
high reduce fraction per mille [900]
initial reduce interval [1e3]
base reduce interval [1e3]
low reduce fraction per mille [500]
stable reluctant doubling restarting [true]
reluctant interval [2^10]
reluctant limit (0=unlimited) [2^20]
reorder decisions (1=stable-mode-only) [2]
initial reorder interval [1e4]
base reorder interval [1e4]
reorder maximum clause size [100]
reinitialization of decision phases [true]
initial rephase interval [1e3]
base rephase interval [1e3]
enable restarts [true]
base restart interval [1]
fast/slow margin in percent [10]

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

random seed [0]
learned clauses (1=bin,2=lrg,3=rec) [3]
enable probing and elimination [true]
small clauses limit [1e5]
enable stable search mode [1]
print complete statistics [false]
equivalent literal substitution [true]
effort in per mille [10]
maximum substitution rounds [2]
subsumption clause size limit [1e3]
subsumption occurrence limit [1e3]
enable SAT sweeping [true]
environment clauses [2^10]
run SAT sweeping until completion [false]
environment depth [2]
effort in per mille [100]
flipping rounds [1]
maximum environment clauses [2^15]
maximum environment depth [3]
maximum environment variables [2^13]
randomize sweeping environment [false]
environment variables [2^8]
target phases (1=stable,2=focused) [1]
learned clause tier one glue limit [2]
relative tier one glue limit [500]
learned clause tier two glue limit [6]
relative tier two glue limit [900]
transitive reduction of binary clauses [true]
effort in per mille [20]
keep transitivity candidates [true]
tumbled external indices order [true]
verbosity level [0]
vivify clauses [true]
effort in per mille [100]

--vivifyfocusedtiers=<bool> use focused tier limits [true]

relative irredundant effort [3]
sort vivification candidates [true]
relative tier1 effort [3]
relative tier2 effort [3]
relative tier3 effort [1]
effort in per mille [50]
initial local search [false]
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.

January 2025 kissat 4.0.2