ACCEPTED PAPERS
SAT 2015 accepted 21 regular papers, 2 short papers and 7 tool papers. The list of accepted papers is also available with abstracts.
Regular papers:
- Alexander Ivrii and Valeriy Balabanov. Speeding up MUS Extraction with Preprocessing and Chunking (details)
- Ruiwen Chen and Rahul Santhanam. Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP (details)
- Jan Burchard, Tobias Schubert and Bernd Becker. Laissez-Faire Caching for Parallel #SAT Solving (details)
- Jonathan Kalechstain, Vadim Ryvchin and Nachum Dershowitz. Hints Revealed (details)
- Alexander Ivrii, Vadim Ryvchin and Ofer Strichman. Mining Backbone Literals In Incremental SAT (details)
- Adam Douglass, Andrew King and Jack Raymond. Constructing SAT filters with a quantum annealer (details)
- Rehan Abdul Aziz, Geoffrey Chu, Christian Muise and Peter J. Stuckey. Projected Model Counting (details)
- Oliver Kullmann and Joao Marques-Silva. Computing maximal autarkies with few and simple oracle queries (details)
- Tomáš Balyo, Peter Sanders and Carsten Sinz. HordeSat: A Massively Parallel Portfolio SAT Solver (details)
- Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl and Bernd Becker. Preprocessing for DQBF (details)
- Simone Bova, Florent Capelli, Stefan Mengel and Friedrich Slivovsky. On Compiling CNFs into Structured Deterministic DNNFs (details)
- Robert Ganian and Stefan Szeider. Community Structure Inspired Algorithms for SAT and #SAT (details)
- Carlos Ansótegui, Jesus Giráldez-Cru, Jordi Levy and Laurent Simon. Using Community Structure to Detect Relevant Learnt Clauses (details)
- Markus Iser, Carsten Sinz and Norbert Manthey. Recognition of Nested Gates in CNF Formulas (details)
- Miguel Neves, Ruben Martins, Mikolas Janota, Ines Lynce and Vasco Manquinho. Exploiting Resolution-based Representations for MaxSAT Solving (details)
- Chanseok Oh. Between SAT and UNSAT: The Fundamental Difference in CDCL SAT (details)
- M. Fareed Arif, Carlos Mencía and Joao Marques-Silva. Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing (details)
- Kuan-Hua Tu, Tzu-Chien Hsu and Jie-Hong Roland Jiang. QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (details)
- Antti E. J. Hyvärinen, Matteo Marescotti and Natasha Sharygina. Search-Space Partitioning for Parallelizing SMT Solvers (details)
- Christian Zielke and Michael Kaufmann. A New Approach to Partial MUS Enumeration (details)
- Armin Biere and Andreas Fröhlich. Evaluating CDCL Variable Scoring Schemes (details)
Short papers:
- Carlos Mencía, Alessandro Previti and Joao Marques-Silva. SAT-Based Horn Least Upper Bounds (details)
- Alexey Ignatiev, Alessandro Previti and Joao Marques-Silva. SAT-Based Formula Simplification (details)
Tool papers:
- Shaowei Cai, Chuan Luo and Kaile Su. CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability (details)
- Peter Steinke and Tobias Philipp. PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF (details)
- Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister and Krzysztof Czarnecki. SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers (details)
- Florian Lonsing and Uwe Egly. Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API (details)
- Stefan Falkner, Marius Lindauer and Frank Hutter. SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers (details)
- Ravi Mangal, Xin Zhang, Aditya Nori and Mayur Naik. Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances (details)
- Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp and Erika Abraham. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (details)