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