CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019

Mate Soos; Armin Biere

CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019

Mate Soos, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings

Abstract

This paper presents the conﬂict-driven clause-learning (CLDL) SAT solver CryptoMiniSat v5.6 (CMS) augmented with the Stochastic Local Search (SLS) [11] solver YalSAT 03v as submitted to SAT Race 2019. CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and ﬁnely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. For the competition, this option was disabled. CryptoMiniSat is authored by Mate Soos. Yet Another Local Search SAT Solver (YalSAT) implements several variants of ProbSAT’s [4] algorithm and recent extensions [3]. These variants are selected randomly at restarts, scheduled by a reluctant doubling scheme (Luby). For further details, see [1]. YalSAT is authored by Armin Biere.

Original language	English
Title of host publication	Proc. of SAT Race 2019 - Solver and Benchmark Descriptions
Editors	Marijn Heule, Matti Järvisalo, Martin Suda
Place of Publication	University of Helsinki
Publisher	Department of Computer Science Series of Publications B
Pages	14-15
Number of pages	2
Volume	B-2019-1
Publication status	Published - 2019

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

Cite this

@inproceedings{5104330ff00e4260b81aabeeab11f5df,

title = "CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019",

abstract = "This paper presents the conﬂict-driven clause-learning (CLDL) SAT solver CryptoMiniSat v5.6 (CMS) augmented with the Stochastic Local Search (SLS) [11] solver YalSAT 03v as submitted to SAT Race 2019. CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and ﬁnely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. For the competition, this option was disabled. CryptoMiniSat is authored by Mate Soos. Yet Another Local Search SAT Solver (YalSAT) implements several variants of ProbSAT{\textquoteright}s [4] algorithm and recent extensions [3]. These variants are selected randomly at restarts, scheduled by a reluctant doubling scheme (Luby). For further details, see [1]. YalSAT is authored by Armin Biere.",

author = "Mate Soos and Armin Biere",

year = "2019",

language = "English",

volume = "B-2019-1",

pages = "14--15",

editor = "\{Marijn Heule, Matti J{\"a}rvisalo, Martin Suda\}",

booktitle = "Proc. of SAT Race 2019 - Solver and Benchmark Descriptions",

publisher = "Department of Computer Science Series of Publications B",

}

CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019. / Soos, Mate; Biere, Armin.
Proc. of SAT Race 2019 - Solver and Benchmark Descriptions. ed. / Marijn Heule, Matti Järvisalo, Martin Suda. Vol. B-2019-1 University of Helsinki: Department of Computer Science Series of Publications B, 2019. p. 14-15.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings

TY - GEN

T1 - CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019

AU - Soos, Mate

AU - Biere, Armin

PY - 2019

Y1 - 2019

N2 - This paper presents the conﬂict-driven clause-learning (CLDL) SAT solver CryptoMiniSat v5.6 (CMS) augmented with the Stochastic Local Search (SLS) [11] solver YalSAT 03v as submitted to SAT Race 2019. CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and ﬁnely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. For the competition, this option was disabled. CryptoMiniSat is authored by Mate Soos. Yet Another Local Search SAT Solver (YalSAT) implements several variants of ProbSAT’s [4] algorithm and recent extensions [3]. These variants are selected randomly at restarts, scheduled by a reluctant doubling scheme (Luby). For further details, see [1]. YalSAT is authored by Armin Biere.

AB - This paper presents the conﬂict-driven clause-learning (CLDL) SAT solver CryptoMiniSat v5.6 (CMS) augmented with the Stochastic Local Search (SLS) [11] solver YalSAT 03v as submitted to SAT Race 2019. CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and ﬁnely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. For the competition, this option was disabled. CryptoMiniSat is authored by Mate Soos. Yet Another Local Search SAT Solver (YalSAT) implements several variants of ProbSAT’s [4] algorithm and recent extensions [3]. These variants are selected randomly at restarts, scheduled by a reluctant doubling scheme (Luby). For further details, see [1]. YalSAT is authored by Armin Biere.

M3 - Conference proceedings

VL - B-2019-1

SP - 14

EP - 15

BT - Proc. of SAT Race 2019 - Solver and Benchmark Descriptions

A2 - Marijn Heule, Matti Järvisalo, Martin Suda, null

PB - Department of Computer Science Series of Publications B

CY - University of Helsinki

ER -