default search action
15th SAT 2012: Trento, Italy
- Alessandro Cimatti, Roberto Sebastiani:
Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Lecture Notes in Computer Science 7317, Springer 2012, ISBN 978-3-642-31611-1
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 S. 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 H. 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 Z. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.