Annals of Mathematics and Artificial Intelligence, Volume 43

Volume 43, Number 1, January 2005

• Franc Brglez, Xiao Yu Li, Matthias F. M. Stallmann:
  On SAT instance classes and a method for reliable performance experiments with SAT solvers. 1-34
  
• Renato Bruni:
  On exact selection of minimally unsatisfiable subformulae. 35-50
  
• Philippe Chapdelaine, Nadia Creignou:
  The complexity of Boolean constraint satisfaction local search problems. 51-63
  
• Eugene Goldberg:
  Testing satisfiability of CNF formulas by computing a stable set of points. 65-89
  
• Edward A. Hirsch, Arist Kojevnikov:
  UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. 91-111
  
• Hans Kleine Büning, Daoyun Xu:
  The complexity of homomorphisms and renamings for minimal unsatisfiable formulas. 113-127
  
• Gabor Kusper:
  Solving the resolution-free SAT problem by submodel propagation in linear time. 129-136
  
• Inês Lynce, João P. Marques Silva:
  Efficient data structures for backtrack search SAT solvers. 137-152
  
• Simona Cocco, Rémi Monasson:
  Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT. 153-172
  
• Stefan Porschen, Bert Randerath, Ewald Speckenmeyer:
  Exact 3-satisfiability is decidable in time O(2^0.16254n). 173-193
  
• Steven David Prestwich, Stéphane Bressan:
  A SAT approach to query optimization in mediator systems. 195-210
  
• Daniele Pretolani:
  Probability logic and optimization SAT: The PSAT and CPA models. 211-221
  
• Stefan Szeider:
  Generalizations of matched CNF formulas. 223-238
  
• Allen Van Gelder:
  Toward leaner binary-clause reasoning in a satisfiability solver. 239-253
  
• Uwe Egly, Reinhard Pichler, Stefan Woltran:
  On deciding subsumption problems. 255-294
  
• Hans Kleine Büning, Xishun Zhao:
  Extension and equivalence problems for clause minimal formulae. 295-306
  
• Laurent Simon, Daniel Le Berre, Edward A. Hirsch:
  The SAT2002 competition. 307-342
  
• Paul W. Purdom, Daniel Le Berre, Laurent Simon:
  A parsimony tree for the SAT2002 competition. 343-365