15. SAT 2012: Trento, Italy

Invited Talks

• Aaron R. Bradley:
  Understanding IC3. 1-14
  
• Donald E. Knuth:
  Satisfiability and The Art of Computer Programming. 15
  

Full Papers

• Adrian Balint, Uwe Schöning:
  Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break. 16-29
  
• Alexandra Goultiaeva, Fahiem Bacchus:
  Off the Trail: Re-examining the CDCL Algorithm. 30-43
  
• Maria Luisa Bonet, Samuel R. Buss:
  An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. 44-57
  
• Friedrich Slivovsky, Stefan Szeider:
  Computing Resolution-Path Dependencies in Linear Time , . 58-71
  
• Serge Gaspers, Stefan Szeider:
  Strong Backdoors to Nested Satisfiability. 72-85
  
• Allen Van Gelder, Samuel B. Wood, Florian Lonsing:
  Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. 86-99
  
• Uwe Egly:
  On Sequent Systems and Resolution for QBFs. 100-113
  
• Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke:
  Solving QBF with Counterexample Guided Refinement. 114-128
  
• Valeriy Balabanov, Hui-Ju Katherine Chiang, Jie-Hong Roland Jiang:
  Henkin Quantifiers and Boolean Formulae. 129-142
  
• Vijay Ganesh, Charles W. O'Donnell, Mate Soos, Srinivas Devadas, Martin C. Rinard, Armando Solar-Lezama:
  Lynx: A Programmatic SAT Solver for the RNA-Folding Problem. 143-156
  
• Krystof Hoder, Nikolaj Bjørner:
  Generalized Property Directed Reachability. 157-171
  
• Stefano Ermon, Ronan LeBras, Carla P. Gomes, Bart Selman, R. Bruce van Dover:
  SMT-Aided Combinatorial Materials Discovery. 172-185
  
• Jian Zhang, Feifei Ma, Zhiqiang Zhang:
  Faulty Interaction Identification via Constraint Solving and Optimization. 186-199
  
• Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette:
  Revisiting Clause Exchange in Parallel SAT Solving. 200-213
  
• Antti Eero Johannes Hyvärinen, Norbert Manthey:
  Designing Scalable Parallel SAT Solvers. 214-227
  
• Lin Xu, Frank Hutter, Holger Hoos, Kevin Leyton-Brown:
  Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors. 228-241
  
• Alexander Nadel, Vadim Ryvchin:
  Efficient SAT Solving under Assumptions. 242-255
  
• Alexander Nadel, Vadim Ryvchin, Ofer Strichman:
  Preprocessing in Incremental SAT. 256-269
  
• Oliver Kullmann, Xishun Zhao:
  On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets. 270-283
  
• António Morgado, Federico Heras, João Marques-Silva:
  Improvements to Core-Guided Binary Search for MaxSAT. 284-297
  
• Anton Belov, Alexander Ivrii, Arie Matsliah, João Marques-Silva:
  On Efficient Computation of Variable MUSes. 298-311
  
• Georg Weissenbacher:
  Interpolant Strength Revisited. 312-326
  
• Dimitris Achlioptas, Ricardo Menchaca-Mendez:
  Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas. 327-340
  
• Nadia Creignou, Heribert Vollmer:
  Parameterized Complexity of Weighted Satisfiability Problems. 341-354
  
• Robert Crowston, Gregory Gutin, Mark Jones, Venkatesh Raman, Saket Saurabh, Anders Yeo:
  Fixed-Parameter Tractability of Satisfying beyond the Number of Variables. 355-368
  
• Matti Järvisalo, Petteri Kaski, Mikko Koivisto, Janne H. Korhonen:
  Finding Efficient Circuits for Ensemble Computation. 369-382
  
• Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä:
  Conflict-Driven XOR-Clause Learning. 383-396
  
• Yael Ben-Haim, Alexander Ivrii, Oded Margalit, Arie Matsliah:
  Perfect Hashing and CNF Encodings of Cardinality Constraints. 397-409
  
• Carlos Ansótegui, Jesús Giráldez-Cru, Jordi Levy:
  The Community Structure of SAT Formulas. 410-423
  
• Thomas Hugel:
  SATLab: X-Raying Random k-SAT - (Tool Presentation). 424-429
  
• Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere:
  Resolution-Based Certificate Extraction for QBF - (Tool Presentation). 430-435
  
• Norbert Manthey:
  Coprocessor 2.0 - A Flexible CNF Simplifier - (Tool Presentation). 436-441
  
• Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám:
  SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). 442-448
  
• Stephan Kottler, Christian Zielke, Paul Seitz, Michael Kaufmann:
  CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers - (Tool Presentation). 449-455
  
• Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara:
  Azucar: A SAT-Based CSP Solver Using Compact Order Encoding - (Tool Presentation). 456-462
  
• Bard Bloom, David Grove, Benjamin Herta, Ashish Sabharwal, Horst Samulowitz, Vijay A. Saraswat:
  SatX10: A Scalable Plug&Play Parallel SAT Framework - (Tool Presentation). 463-468
  
• Ashutosh Gupta:
  Improved Single Pass Algorithms for Resolution Proof Reduction - (Poster Presentation). 469-470
  
• Sebastian Burg, Stephan Kottler, Michael Kaufmann:
  Creating Industrial-Like SAT Instances by Clustering and Reconstruction - (Poster Presentation). 471-472
  
• Paolo Marin, Christian Miller, Bernd Becker:
  Incremental QBF Preprocessing for Partial Design Verification - (Poster Presentation). 473-474
  
• Peter van der Tak, Marijn Heule, Armin Biere:
  Concurrent Cube-and-Conquer - (Poster Presentation). 475-476
  
• Chu Min Li, Yu Li:
  Satisfying versus Falsifying in Local Search for Satisfiability - (Poster Presentation). 477-478
  
• Chu Min Li, Wanxia Wei, Yu Li:
  Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability - (Poster Presentation). 479-480
  
• Alejandro Arbelaez, Philippe Codognet:
  Towards Massively Parallel Local Search for SAT - (Poster Presentation). 481-482
  
• Markus Iser, Mana Taghdiri, Carsten Sinz:
  Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod - (Poster Presentation). 483-484
  
• Mark H. Liffiton, Jordyn C. Maglalang:
  A Cardinality Solver: More Expressive Constraints for Free - (Poster Presentation). 485-486
  
• Sam Bayless, Alan J. Hu:
  Single-Solver Algorithms for 2QBF - (Poster Presentation). 487-488
  
• Emir Demirovic, Haris Gavranovic:
  An Efficient Method for Solving UNSAT 3-SAT and Similar Instances via Static Decomposition - (Poster Presentation). 489-490
  
• Saïd Jabbour, Jerry Lonlac, Lakhdar Saïs:
  Intensification Search in Modern SAT Solvers - (Poster Presentation). 491-492
  
• Iago Abal, Alcino Cunha, Joe Hurd, Jorge Sousa Pinto:
  Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation). 493-495
  
• George Katsirelos, Laurent Simon:
  Learning Polynomials over GF(2) in a SAT Solver - (Poster Presentation). 496-497
  
• Ashish Sabharwal, Horst Samulowitz, Meinolf Sellmann:
  Learning Back-Clauses in SAT - (Poster Presentation). 498-499
  
• Arie Matsliah, Ashish Sabharwal, Horst Samulowitz:
  Augmenting Clause Learning with Implied Literals - (Poster Presentation). 500-501
  

Last update Thu May 23 03:55:43 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page