Theory and Applications of Satisfiability Testing – SAT 2018

Description

This book constitutes the refereed proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018, held in Oxford, UK, in July 2018. The 20 revised full papers, 4 short papers, and 2 tool papers were carefully reviewed and selected from 58 submissions. The papers address different aspects of SAT interpreted in a broad sense, including theoretical advances (such as exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications as well as case studies and reports on findings based on rigorous experimentation. They are organized in the following topical sections: maximum satisfiability; conflict driven clause learning; model counting; quantified Boolean formulae; theory; minimally unsatisfiable sets; satisfiability modulo theories; and tools and applications. Front Matter ....Pages I-XIX Front Matter ....Pages 1-1 Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (Christoph Scholl, Ralf Wimmer)....Pages 3-16 Front Matter ....Pages 17-17 Approximately Propagation Complete and Conflict Propagating Constraint Encodings (Rüdiger Ehlers, Francisco Palau Romero)....Pages 19-36 Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (Tobias Paxian, Sven Reimer, Bernd Becker)....Pages 37-53 Solving MaxSAT with Bit-Vector Optimization (Alexander Nadel)....Pages 54-72 Front Matter ....Pages 73-73 Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, Marc Vinyals)....Pages 75-93 Machine Learning-Based Restart Policy for CDCL SAT Solvers (Jia Hui Liang, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, Vijay Ganesh)....Pages 94-110 Chronological Backtracking (Alexander Nadel, Vadim Ryvchin)....Pages 111-121 Centrality-Based Improvements to CDCL Heuristics (Sima Jamali, David Mitchell)....Pages 122-131 Front Matter ....Pages 133-133 Fast Sampling of Perfectly Uniform Satisfying Assignments (Dimitris Achlioptas, Zayd S. Hammoudeh, Panos Theodoropoulos)....Pages 135-147 Fast and Flexible Probabilistic Model Counting (Dimitris Achlioptas, Zayd Hammoudeh, Panos Theodoropoulos)....Pages 148-164 Exploiting Treewidth for Projected Model Counting and Its Limits (Johannes K. Fichte, Markus Hecher, Michael Morak, Stefan Woltran)....Pages 165-184 Front Matter ....Pages 185-185 Circuit-Based Search Space Pruning in QBF (Mikoláš Janota)....Pages 187-198 Symmetries of Quantified Boolean Formulas (Manuel Kauers, Martina Seidl)....Pages 199-216 Local Soundness for QBF Calculi (Martin Suda, Bernhard Gleiss)....Pages 217-234 QBF as an Alternative to Courcelle’s Theorem (Michael Lampis, Stefan Mengel, Valia Mitsou)....Pages 235-252 Polynomial-Time Validation of QCDCL Certificates (Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider)....Pages 253-269 Front Matter ....Pages 271-271 Sharpness of the Satisfiability Threshold for Non-uniform Random k-SAT (Tobias Friedrich, Ralf Rothenberger)....Pages 273-291 In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (Marc Vinyals, Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström)....Pages 292-310 Cops-Robber Games and the Resolution of Tseitin Formulas (Nicola Galesi, Navid Talebanfard, Jacobo Torán)....Pages 311-326 Front Matter ....Pages 327-327 Minimal Unsatisfiability and Minimal Strongly Connected Digraphs (Hoda Abbasizanjani, Oliver Kullmann)....Pages 329-345 Finding All Minimal Safe Inductive Sets (Ryan Berryhill, Alexander Ivrii, Andreas Veneris)....Pages 346-362 Front Matter ....Pages 363-363 Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition (Shubhani Gupta, Aseem Saxena, Anmol Mahajan, Sorav Bansal)....Pages 365-382 Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani)....Pages 383-398 Front Matter ....Pages 399-399 XOR-Satisfiability Set Membership Filters (Sean A. Weaver, Hannah J. Roberts, Michael J. Smith)....Pages 401-418 ALIAS: A Modular Tool for Finding Backdoors for SAT (Stepan Kochemazov, Oleg Zaikin)....Pages 419-427 PySAT: A Python Toolkit for Prototyping with SAT Oracles (Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva)....Pages 428-437 Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner, Mooly Sagiv)....Pages 438-449 Back Matter ....Pages 451-452