Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction

DOI10.1007/978-3-642-39071-5_23zbMath1390.68587OpenAlexW1511069520MaRDI QIDQ5326472

Jean-Marie Lagniez, Laurent Simon, Gilles Audemard

Publication date: 5 August 2013

Published in: Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39071-5_23

Mathematics Subject Classification ID

Related Items (22)

Multi-agent pathfinding with continuous time ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ SAT-Based Formula Simplification ⋮ SAT-Based Horn Least Upper Bounds ⋮ SAT race 2015 ⋮ Conformant planning as a case study of incremental QBF solving ⋮ The first international competition on computational models of argumentation: results and analysis ⋮ Combining incomplete search and clause generation: an application to the orienteering problems with time windows ⋮ Search of fractal space-filling curves with minimal dilation ⋮ Propositional proof systems based on maximum satisfiability ⋮ Minimal self-similar Peano curve of genus \(5 \times 5\) ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ New models for generating hard random Boolean formulas and disjunctive logic programs ⋮ Definability for model counting ⋮ On orthogonal symmetric chain decompositions ⋮ Multi-agent path finding with mutex propagation ⋮ On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving ⋮ RC2: an Efficient MaxSAT Solver ⋮ Learning Optimal Decision Sets and Lists with SAT ⋮ SAT-based rigorous explanations for decision lists ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT ⋮ The \textsc{MergeSat} solver

Uses Software

• Chaff
• Glucose
• AMUSE
• Velev SAT Benchmarks

This page was built for publication: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction