The \textsc{MergeSat} solver

DOI10.1007/978-3-030-80223-3_27MaRDI QIDQ2118329zbMATH OpenOpenAlexFDO

Authors Norbert Manthey

Publication date 22 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-80223-3_27

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07)

Recommendations

• The \(Multi\)-SAT algorithm
• Theory and Applications of Satisfiability Testing
• A synthesis of constraint satisfaction and constraint solving
• Integrating algebraic and SAT solvers
• ManySAT: a parallel SAT solver
• Theory and Applications of Satisfiability Testing
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• Combining preorder and postorder resolution in a satisfiability solver

Cites work

• Between SAT and UNSAT: the fundamental difference in CDCL SAT
• Chronological backtracking
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Empirical study of the anatomy of modern SAT solvers
• HordeSat: a massively parallel portfolio SAT solver
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Improving implementation of SAT competitions 2017--2019 winners
• Improving resource-unaware SAT solvers
• Kissat
• Open-WBO: a modular MaxSAT solver
• Paracooba
• Paramils: an automatic algorithm configuration framework
• Reusing the assignment trail in CDCL solvers
• SAT race 2015
• Speeding up assumption-based SAT
• SpyBug: automated bug detection in the configuration space of SAT solvers
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Trail saving on backtrack

Cited in

(2)

• MergeSat
• MedleySolver: online SMT algorithm selection

Describes a project that uses

Uses Software

• MiniSat
• Paramils
• Valgrind
• Plingeling
• PrecoSAT
• Glucose
• CBMC
• Open-WBO
• Treengeling
• HordeSat
• Spybug
• COMiniSatPS
• Travis CI
• Lingeling
• MapleCOMSPS
• MapleCOMSPS_LRB
• YalSAT
• CaDiCaL
• GitHub
• Maple_LCM_Dist_ChronoBT
• Paracooba
• Kissat

This page was built for publication: The \textsc{MergeSat} solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2118329)