Journal of Automated Reasoning (JAR), Volume 35

Volume 35, Numbers 1-3, October 2005

• Enrico Giunchiglia, Toby Walsh:
  Satisfiability in the Year 2005. 1-2
  
• Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva:
  Heuristic-Based Backtracking Relaxation for Propositional Satisfiability. 3-24
  
• Guoqiang Pan, Moshe Y. Vardi:
  Symbolic Techniques in Satisfiability Solving. 25-50
  
• Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson:
  Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas. 51-72
  
• Stefan Szeider:
  Backdoor Sets for DLL Subsolvers. 73-88
  
• Jan Johannsen:
  The Complexity of Pure Literal Elimination. 89-95
  
• John Thornton:
  Clause Weighting Local Search for SAT. 97-142
  
• Alan M. Frisch, Timothy J. Peugniez, Anthony J. Doggett, Peter Nightingale:
  Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. 143-179
  
• Yacine Boufkhad, Olivier Dubois, Yannet Interian, Bart Selman:
  Regular Random k-SAT: Properties of Balanced Formulas. 181-200
  
• Andreas Meier, Volker Sorge:
  Applying SAT Solving in Classification of Finite Algebras. 201-235
  
• Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Marco Maratea:
  The SAT-based Approach to Separation Logic. 237-263
  
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
  MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. 265-293
  

Volume 35, Number 4, November 2005

• Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa:
  Tool-Assisted Specification and Verification of Typed Low-Level Languages. 295-354
  
• Robert S. Boyer, Wilfred J. Legato, Victor W. Marek:
  Toward Automating the Discovery of Decreasing Measures. 355-371
  
• Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump:
  Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). 373-390
  
• Nicolas Peltier:
  Some Techniques for Proving Termination of the Hyperresolution Calculus. 391-427
  
• Nimish Shah:
  "Rippling: Meta-Level Guidance for Mathematical Reasoning, " by Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland, Cambridge University Press, 2005. 429-431