SLIME

A Free World Class High Performance SAT Solver

SLIME Cloud: A Free Massive World Class High Performance SAT Solver.

Winner of Crypto Track and 3rd place on Cloud Track at the SAT Competition 2021

https://github.com/maxtuno/SLIME

SLIME CLI & SLIME CLOUD

Currently the best SAT Solver, several light years around.

SLIME CLI

Kissat-sc2020 vs SLIME 5 at 10.000 seconds

Anonymous Link to Report

SLIME 5

PAR-2 Score 1499518.553

Solved 192 = SAT 131 + UNSAT 61

Kissat-sc2020: http://fmv.jku.at/kissat/

PAR-2 Score 1564281.3671

Solved 185 = SAT 115 + UNSAT 71

SLIME 5 Cloud: A Free Massive World Class High Performance SAT Solver.

SLIME 5: The Unofficial State of The Art

SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf)

SLIME 3.1.1: The Unofficial State of The Art

CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1 CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1 CaDiCaL vs MapleLCMDiscChronoBT-DL-v3 vs SLIME 3.1.1

SLIME 3.1: The Unofficial State of The Art

SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf)

SLIME 3.0: The Unofficial State of The Art

SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf) SAT Race 2019 (Secondhalf) SAT Race 2006

SLIME 2.2: A Free World Class Multiplatform High Performance SAT Solver

SLIME 2.1: A Free World Class High Performance SAT Solver

SLIME 2.0: A Free World Class High Performance SAT Solver

SAT Race 2015

(The solvers will ranked using the PAR-2 scheme: The score of a solver is defined as the sum of all runtimes for solved instances + 2*timeout for unsolved instances, lowest score wins.) SAT Race 2006 SAT Race 2015 SAT Race 2006

SLIME: A Minimal Heuristic to Boost SAT Solving


On CDCL Based SAT Solvers the trail size is strictly related to progress or to the total conflicts on the current assignment, such that if the trail size is the same that the number of variables, then current assignment is valid. On the other hand, in the selection of the current variable it is necessary to assign a predetermined polarity to the resulting literal, which in most implementations is a predefined value. SLIME implement a simple heuristic with minimal complexity, that correlated the trail size and the polarity of the current variable to assign. The selection of variable is not related to trail size, this decouple the both concepts.