


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 - Ashlin 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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














