Release 4.0.4

Version 4.0.4

• removed a quadratic ITE gate extraction issue in congruence
• fixes for kitten stand-alone usage
• disabled fast elimination fastel by default
• delayed bounded variable addition factor for larger formulas

Release 4.0.3

• reversed VMTF and heap order of factored variables aka BVA
• properly checking and fixed VMTF stamping order after factoring
• added -flto support / test (reason for changes to stack)
• reactivated scripts/build-and-test-all-configurations.sh
• inlined through macros generic stack enlarging / shrinking

rel-4.0.2

Version 4.0.2

• support for setting printing prefix 'kissat_prefix'

Release 4.0.1

Version 4.0.1

• updated README to point to the 2024 system description
• removed redundant line in congruence closure
• fixed proof chain generation for matching ITE
• fixed getting size of watches for --compact
• more precise completion in congruence
• writing DIMACS to <stdout> with -o -
• fixed reporting in congruence
• fixed DIMACS writing

Release 4.0.0

This is the version submitted to the SAT Competition 2024.

It was dominating the competition and won first places, i.e., 3 gold medals, in the categories of the main track (SAT, UNSAT, SAT+UNSAT).

Release 3.1.1

Version 3.1.1

• configuration option --safe disables writing through popen

Release 3.1.0

This is the version submitted to the SAT Competition 2023.

For the Apple binaries you might get an error when trying to run the unzipped file after downloading with Safari.
This quarantine apparently can be removed with

xattr -d com.apple.quarantine kissat-3.1.0-apple-arm64

after unzipping the downloaded file. You can also just download through wget.
If you are worried about forcing quarantine removal, I would suggest try to build from source code.

Release 3.0.0

First release after SAT Competition 2022 Light Version

SAT Competition 2022 Light Release

sc2022-light

imported sc2022-light

SAT Competition 2022 Hyper Release

sc2022-hyper

imported sc2022-hyper