| Description |
1 online resource |
| Series |
Lecture notes in computer science, 0302-9743 ; 7317 |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 7317.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
Understanding IC3 / Aaron R. Bradley -- Satisfiability and The Art of Computer Programming / Donald Knuth -- Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break / Adrian Balint and Uwe Schöning -- Off the Trail: Re-examining the CDCL Algorithm / Alexandra Goultiaeva and Fahiem Bacchus -- An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning / Maria Luisa Bonet and Sam Buss -- Computing Resolution-Path Dependencies in Linear Time, / Friedrich Slivovsky and Stefan Szeider -- Strong Backdoors to Nested Satisfiability / Serge Gaspers and Stefan Szeider -- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas / Allen Van Gelder, Samuel B. Wood and Florian Lonsing -- On Sequent Systems and Resolution for QBFs / Uwe Egly -- Solving QBF with Counterexample Guided Refinement / Mikoláš Janota, William Klieber, Joao Marques-Silva and Edmund Clarke -- Henkin Quantifiers and Boolean Formulae / Valeriy Balabanov, Hui-Ju Katherine Chiang and Jie-Hong Roland Jiang -- Lynx: A Programmatic SAT Solver for the RNA-Folding Problem / Vijay Ganesh, Charles W. O'Donnell, Mate Soos, Srinivas Devadas and Martin C. Rinard, et al. -- Generalized Property Directed Reachability / Kryštof Hoder and Nikolaj Bjørner -- SMT-Aided Combinatorial Materials Discovery / Stefano Ermon, Ronan Le Bras, Carla P. Gomes, Bart Selman and R. Bruce van Dover -- Faulty Interaction Identification via Constraint Solving and Optimization / Jian Zhang, Feifei Ma and Zhiqiang Zhang |
|
Revisiting Clause Exchange in Parallel SAT Solving / Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez and Cédric Piette -- Designing Scalable Parallel SAT Solvers / Antti E.J. Hyvärinen and Norbert Manthey -- Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors / Lin Xu, Frank Hutter, Holger Hoos and Kevin Leyton-Brown -- Efficient SAT Solving under Assumptions / Alexander Nadel and Vadim Ryvchin -- Preprocessing in Incremental SAT / Alexander Nadel, Vadim Ryvchin and Ofer Strichman -- On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets / Oliver Kullmann and Xishun Zhao -- Improvements to Core-Guided Binary Search for MaxSAT / Antonio Morgado, Federico Heras and Joao Marques-Silva -- On Efficient Computation of Variable MUSes / Anton Belov, Alexander Ivrii, Arie Matsliah and Joao Marques-Silva -- Interpolant Strength Revisited / Georg Weissenbacher -- Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas / Dimitris Achlioptas and Ricardo Menchaca-Mendez -- Parameterized Complexity of Weighted Satisfiability Problems / Nadia Creignou and Heribert Vollmer -- Fixed-Parameter Tractability of Satisfying beyond the Number of Variables / Robert Crowston, Gregory Gutin, Mark Jones, Venkatesh Raman and Saket Saurabh, et al. -- Finding Efficient Circuits for Ensemble Computation / Matti Järvisalo, Petteri Kaski, Mikko Koivisto and Janne H. Korhonen -- Conflict-Driven XOR-Clause Learning / Tero Laitinen, Tommi Junttila and Ilkka Niemelä |
|
Perfect Hashing and CNF Encodings of Cardinality Constraints / Yael Ben-Haim, Alexander Ivrii, Oded Margalit and Arie Matsliah -- The Community Structure of SAT Formulas / Carlos Ansótegui, Jesús Giráldez-Cru and Jordi Levy -- SATLab: X-Raying Random k-SAT (Tool Presentation) / Thomas Hugel -- Resolution-Based Certificate Extraction for QBF (Tool Presentation) / Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl and Armin Biere -- Coprocessor 2.0 -- A Flexible CNF Simplifier (Tool Presentation) / Norbert Manthey -- SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox (Tool Presentation) / Florian Corzilius, Ulrich Loup, Sebastian Junges and Erika Ábrahám -- CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers (Tool Presentation) / Stephan Kottler, Christian Zielke, Paul Seitz and Michael Kaufmann -- Azucar: A SAT-Based CSP Solver Using Compact Order Encoding (Tool Presentation) / Tomoya Tanjo, Naoyuki Tamura and Mutsunori Banbara -- SatX10: A Scalable Plug & Play Parallel SAT Framework (Tool Presentation) / Bard Bloom, David Grove, Benjamin Herta, Ashish Sabharwal and Horst Samulowitz, et al. -- Improved Single Pass Algorithms for Resolution Proof Reduction (Poster Presentation) / Ashutosh Gupta -- Creating Industrial-Like SAT Instances by Clustering and Reconstruction (Poster Presentation) / Sebastian Burg, Stephan Kottler and Michael Kaufmann -- Incremental QBF Preprocessing for Partial Design Verification (Poster Presentation) / Paolo Marin, Christian Miller and Bernd Becker -- Concurrent Cube-and-Conquer (Poster Presentation) / Peter van der Tak, Marijn J.H. Heule and Armin Biere |
|
Satisfying versus Falsifying in Local Search for Satisfiability (Poster Presentation) / Chu Min Li and Yu Li -- Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability (Poster Presentation) / Chu Min Li, Wanxia Wei and Yu Li -- Towards Massively Parallel Local Search for SAT (Poster Presentation) / Alejandro Arbelaez and Philippe Codognet -- Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod (Poster Presentation) / Markus Iser, Mana Taghdiri and Carsten Sinz -- A Cardinality Solver: More Expressive Constraints for Free (Poster Presentation) / Mark H. Liffiton and Jordyn C. Maglalang -- Single-Solver Algorithms for 2QBF (Poster Presentation) / Sam Bayless and Alan J. Hu -- An Efficient Method for Solving UNSAT 3-SAT and Similar Instances via Static Decomposition (Poster Presentation) / Emir Demirović and Haris Gavranović -- Intensification Search in Modern SAT Solvers (Poster Presentation) / Saïd Jabbour, Jerry Lonlac and Lakhdar Saïs -- Using Term Rewriting to Solve Bit-Vector Arithmetic Problems (Poster Presentation) / Iago Abal, Alcino Cunha, Joe Hurd and Jorge Sousa Pinto -- Learning Polynomials over GF(2) in a SAT Solver (Poster Presentation) / George Katsirelos and Laurent Simon -- Learning Back-Clauses in SAT (Poster Presentation) / Ashish Sabharwal, Horst Samulowitz and Meinolf Sellmann -- Augmenting Clause Learning with Implied Literals (Poster Presentation) / Arie Matsliah, Ashish Sabharwal and Horst Samulowitz |
| Summary |
Annotation This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings |
| Analysis |
Computer science |
|
Computer software |
|
Logic design |
|
Artificial intelligence |
|
Logics and Meanings of Programs |
|
Computation by Abstract Devices |
|
Algorithm Analysis and Problem Complexity |
|
Mathematical Logic and Formal Languages |
|
Information and Communication, Circuits |
| Bibliography |
Includes bibliographical references and author index |
| Subject |
Computer algorithms -- Congresses
|
|
Computer software -- Verification -- Congresses
|
|
Informatique.
|
|
Computer algorithms
|
|
Computer software -- Verification
|
| Genre/Form |
Conference papers and proceedings
|
|
Software.
|
| Form |
Electronic book
|
| Author |
Cimatti, Alessandro.
|
|
Sebastiani, R. (Roberto)
|
| ISBN |
9783642316128 |
|
3642316123 |
|
3642316115 |
|
9783642316111 |
|
