Abstract is missing.
- The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic ProofsAlbert Atserias. 1-17 [doi]
- Turing's Computable Real Numbers and Why They Are Still Important TodayEdmund M. Clarke. 18 [doi]
- There Are No CNF ProblemsPeter J. Stuckey. 19-21 [doi]
- Soundness of Inprocessing in Clause Sharing SAT SolversNorbert Manthey, Tobias Philipp, Christoph Wernhard. 22-39 [doi]
- Exponential Separations in a Hierarchy of Clause Learning Proof SystemsJan Johannsen. 40-51 [doi]
- On the Resolution Complexity of Graph Non-isomorphismJacobo Torán. 52-66 [doi]
- On Propositional QBF Expansions and Q-ResolutionMikolás Janota, Joao Marques-Silva. 67-82 [doi]
- Recovering and Utilizing Partial Duality in QBFAlexandra Goultiaeva, Fahiem Bacchus. 83-99 [doi]
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit PropagationFlorian Lonsing, Uwe Egly, Allen Van Gelder. 100-115 [doi]
- Concurrent Clause StrengtheningSiert Wieringa, Keijo Heljanko. 116-132 [doi]
- Parallel MUS ExtractionAnton Belov, Norbert Manthey, Joao Marques-Silva. 133-149 [doi]
- A Modular Approach to MaxSAT Modulo TheoriesAlessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani. 150-165 [doi]
- Exploiting the Power of mip Solvers in maxsatJessica Davies, Fahiem Bacchus. 166-181 [doi]
- Community-Based Partitioning for MaxSAT SolvingRuben Martins, Vasco M. Manquinho, Inês Lynce. 182-191 [doi]
- Experiments with Reduction FindingCharles Jordan, Lukasz Kaiser. 192-207 [doi]
- A Constraint Satisfaction Approach for Programmable Logic Detailed PlacementAndrew Mihal, Steve Teig. 208-223 [doi]
- Minimizing Models for Tseitin-Encoded SAT InstancesMarkus Iser, Carsten Sinz, Mana Taghdiri. 224-232 [doi]
- Solutions for Hard and Soft Constraints Using Optimized Probabilistic SatisfiabilityMarcelo Finger, Ronan LeBras, Carla P. Gomes, Bart Selman. 233-249 [doi]
- Quantified Maximum Satisfiability: - A Core-Guided ApproachAlexey Ignatiev, Mikolás Janota, Joao Marques-Silva. 250-266 [doi]
- Nested Boolean Functions as Models for Quantified Boolean FormulasUwe Bubeck, Hans Kleine Büning. 267-275 [doi]
- Factoring Out Assumptions to Speed Up MUS ExtractionJean-Marie Lagniez, Armin Biere. 276-292 [doi]
- On the Interpolation between Product-Based Message Passing Heuristics for SATOliver Gableske. 293-308 [doi]
- Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS ExtractionGilles Audemard, Jean-Marie Lagniez, Laurent Simon. 309-317 [doi]
- A SAT Approach to Clique-WidthMarijn Heule, Stefan Szeider. 318-334 [doi]
- Cliquewidth and Knowledge CompilationIgor Razgon, Justyna Petke. 335-350 [doi]
- A Rank Lower Bound for Cutting Planes Proofs of Ramsey's TheoremMassimo Lauria. 351-364 [doi]
- The Complexity of Theorem Proving in Autoepistemic LogicOlaf Beyersdorff. 365-376 [doi]
- Local BackbonesRonald de Haan, Iyad A. Kanj, Stefan Szeider. 377-393 [doi]
- Upper and Lower Bounds for Weak Backdoor Set DetectionNeeldhara Misra, Sebastian Ordyniak, Venkatesh Raman, Stefan Szeider. 394-402 [doi]
- LearnSAT: A SAT Solver for EducationMordechai Ben-Ari. 403-407 [doi]
- MUStICCa: MUS Extraction with Interactive Choice of CandidatesJohannes Dellert, Christian Zielke, Michael Kaufmann. 408-414 [doi]
- SCSat: A Soft Constraint Guided SAT SolverHiroshi Fujita, Miyuki Koshimura, Ryuzo Hasegawa. 415-421 [doi]
- Snappy: A Simple Algorithm PortfolioHorst Samulowitz, Chandra Reddy, Ashish Sabharwal, Meinolf Sellmann. 422-428 [doi]
- Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming SystemsTakehide Soh, Naoyuki Tamura, Mutsunori Banbara. 429-436 [doi]