SAT competition 2020
type: Item
instance of: scholarly article
title: SAT competition 2020
zbMATH Open document ID: 1478.68320
author: Nils Froleyks
author: Marijn J. H. Heule
author: Markus Iser
author: Matti Järvisalo
author: Martin Suda
published in: Artificial Intelligence
publication date: 2021-12-13T00:00:00Z
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68R07
zbMATH DE Number: 7443156
zbMATH Keywords: SAT
zbMATH Keywords: Boolean satisfiability
zbMATH Keywords: SAT competition
zbMATH Keywords: SAT solvers
zbMATH Keywords: empirical evaluation
zbMATH Keywords: benchmarking
describes a project that uses: YalSAT
describes a project that uses: DRAT-trim
describes a project that uses: Treengeling
describes a project that uses: HordeSat
describes a project that uses: Paracooba
describes a project that uses: cake_lpr
describes a project that uses: SLIME
describes a project that uses: Kissat
describes a project that uses: z3
describes a project that uses: StarExec
describes a project that uses: Coprocessor
describes a project that uses: PaInleSS
describes a project that uses: ManySAT
describes a project that uses: Plingeling
describes a project that uses: PBLib
describes a project that uses: Lingeling
describes a project that uses: CaDiCaL
describes a project that uses: MapleCOMSPS_LRB
describes a project that uses: MapleCOMSPS
MaRDI profile type: Publication
full work available at URL: j.artint.2021.103572
OpenAlex ID: W3193251185
cites work: Q5148371
cites work: Theory and Applications of Satisfiability Testing
cites work: SAT race 2015
cites work: Temporal induction by incremental SAT solving
cites work: Ultimately Incremental SAT
cites work: Incremental inprocessing in SAT solving
cites work: Computer Aided Verification
cites work: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
cites work: Planning as satisfiability: parallel plans and algorithms for plan search
cites work: Q3624014
cites work: Determining computational complexity from characteristic ‘phase transitions’
cites work: Algorithms for computing backbones of propositional formulae
cites work: PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
cites work: Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
cites work: Learning Rate Based Branching Heuristic for SAT Solvers
cites work: Chronological backtracking
cites work: CrystalBall: gazing in the black box of SAT solving
cites work: Clause vivification by unit propagation in CDCL SAT solvers
cites work: Truth Assignments as Conditional Autarkies
cites work: Designing new phase selection heuristics
cites work: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling
cites work: Improved Static Symmetry Breaking for SAT
cites work: Trail saving on backtrack
cites work: HordeSat: A Massively Parallel Portfolio SAT Solver
cites work: Concurrent Clause Strengthening
cites work: Lazy Clause Exchange Policy for Parallel SAT Solvers
cites work: Q3639756
cites work: Scalable SAT solving in the cloud
cites work: Q2479551
DOI: 10.1016/J.ARTINT.2021.103572
description: scientific article; zbMATH DE number 7443156