Volume 1 Contents

Download all articles from this volume


Miguel F. Anjos. Semidefinite Optimization Approaches for Satisfiability and Maximum-Satisfiability Problems. Volume 1 (2005), pages 1-47.
  • Keywords: satisfiability, maximum-satisfiability, semidefinite programming, semidefinite optimization, approximation algorithms, semidefinite relaxations, lifting procedures.
  • PDF

Evgeny Dantsin and Alexander Wolpert. A Faster Clause-Shortening Algorithm for SAT with No Restriction on Clause Length. Volume 1 (2005), pages 49-60.
  • Keywords: SAT with no restriction on clause length, upper bound, clause shortening.
  • PDF

Sylvie Coste-Marquis, Daniel Le Berre, Florian Letombe, and Pierre Marquis. Complexity Results for Quantified Boolean Formulae Based on Complete Propositional Languages. Volume 1 (2006), pages 61-88.
  • Keywords: automated reasoning, quantified Boolean formulae.
  • PDF

Sean Weaver, John Franco, and John Schlipf. Extending Existential Quantification in Conjunctions of BDDs. Volume 1 (2006), pages 89-110.
  • Keywords: satisfiability, autarky, safe assignment, inference.
  • PDF

Daniel Rolf. Improved Bound for the PPSZ/Schöning-Algorithm for 3-SAT. Volume 1 (2006), pages 111-122.
  • Keywords: 3-SAT, worst case bound, bounded resolution, randomized local search.
  • PDF


Eliezer L. Lozinskii. Impurity: Another Phase Transition of SAT. Volume 1 (2006), research note, pages 123-141.
  • Keywords: SAT, phase transition, impurity.
  • PDF

Konstantin Kutzkov. A Note on the Use of Independent Sets for the k-SAT Problem. Volume 1 (2007), research note, pages 143-145.
  • Keywords: k-SAT problem, upper bounds, independent sets of variables.
  • PDF

Special Issue on SAT/CP Integration
Editors: Youssef Hamadi and Lucas Bordeaux


Youssef Hamadi and Lucas Bordeaux. Preface.
Christophe Lecoutre, Lakhdar Saïs, Sébastien Tabary, and Vincent Vidal. Recording and Minimizing Nogoods from Restarts. Volume 1 (2007), pages 147-167.
  • Keywords: learning, watched literals, restarts, CSP.
  • PDF

Christophe Lecoutre, Lakhdar Saïs, and Julien Vion. Using SAT Encodings to Drive CSP Value Ordering Heuristics. Volume 1 (2007), pages 169-186.
  • Keywords: heuristics, SAT encodings, CSP.
  • PDF

Shuvendu K. Lahiri and Krishna K. Mehra. Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic. Volume 1 (2007), pages 187-207.
  • Keywords: SAT-solver, interpolants, decision procedures, linear arithmetic, satisfiability modulo theories.
  • PDF

Martin Fränzle, Cristian Herde, Tino Teige, Stefan Ratschan, and Tobias Schubert. Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure. Volume 1 (2007), pages 209-236.
  • Keywords: interval-based arithmetic constraint solving, SAT modulo theories.
  • PDF