SAT race 2015

DOI10.1016/J.ARTINT.2016.08.007zbMATH Open1392.68381DBLPjournals/ai/BalyoBIS16OpenAlexW2508838091WikidataQ59065435 ScholiaQ59065435MaRDI QIDQ334795FDOQ334795

Authors: Tomáš Balyo, Armin Biere, Markus Iser, Carsten Sinz 

Publication date: 1 November 2016

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2016.08.007

Recommendations

• SAT competition 2020
• The state of SAT
• Improving implementation of SAT competitions 2017--2019 winners
• scientific article; zbMATH DE number 5139160
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 956858
• scientific article; zbMATH DE number 5139164

zbMATH Keywords

competitionSATSAT solvers

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites Work

• ManySAT: a parallel SAT solver
• Theory and Applications of Satisfiability Testing
• PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
• Recognition of Nested Gates in CNF Formulas
• Title not available (Why is that?)
• The complexity of theorem-proving procedures
• Title not available (Why is that?)
• GRASP: a search algorithm for propositional satisfiability
• Optimal speedup of Las Vegas algorithms
• Inprocessing rules
• Blocked Clause Decomposition
• Lazy Clause Exchange Policy for Parallel SAT Solvers
• Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
• Automated Benchmarking of Incremental SAT and QBF Solvers
• Blocked clause elimination
• Title not available (Why is that?)
• Improving resource-unaware SAT solvers
• Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
• Theorem proving using lazy proof explication.

Cited In (9)

• Consistency checking of STNs with decisions: managing temporal and access-control constraints in a seamless way
• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• On black-box optimization in divide-and-conquer SAT solving
• Theory and Applications of Satisfiability Testing
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems
• The \textsc{MergeSat} solver
• SAT competition 2020

Uses Software

• ManySAT
• MiniSat
• Chaff
• Plingeling
• Glucose
• DIMACS
• StarExec
• Treengeling
• PBLib
• COMiniSatPS
• abcdSAT
• Lingeling
• cnf2aig

This page was built for publication: SAT race 2015

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