Topics related to Knowledge Representation, Constraint Satisfaction, and Self-Adaptive Algorithms

In particular, I am interested in projects centered on the Satisfiability Problem (SAT and #SAT) and Quantified Boolean Formulas (QBF). In addition, all generalizations like Model Counting (#SAT, #QBF), QCSPs (Quantified Constraint Satisfaction Problems), and SCSP (Stochastic Constraint Satisfaction Problems) are of interest.
Recently, I am also exploiting machine learning techniques in order to improve the performance of algorithms by dynamically adapting the solving strategy depending on the current problem characteristics.

Solving Quantified Boolean Formulas (pdf) , University of Toronto, 2008

Committee: Fahiem Bacchus, Hector Levesque, Toni Pitassi, Sheila McIlraith, External Examiner: Bart Selman

• Learning to Solve QBF (pdf paper)
  Horst Samulowitz and Roland Memisevic
  published in AAAI 2007 (Twenty-Second Conference on Artificial Intelligence), 2007.
  
  
• Solution Backjumping for #SAT (short paper)
  Jessica Davies and Eric Hsu and Horst Samulowitz
  published in NESCAI 2007 (North East Student Colloquium on Artificial Intelligence), 2007
  
  
• Dynamically Partitioning for Solving QBF (pdf paper)
  Horst Samulowitz and Fahiem Bacchus
  published in SAT 2007 (Tenth International Conference on Theory and Applications of Satisfiability Testing), 2007.
  
  
• On the Stochastic Constraint Satisfaction Framework (pdf paper)
  Lucas Bordeaux and Horst Samulowitz
  published in SAC 2007 (The 22nd Annual ACM Symposium on Applied Computing) , 2007.
  
  
• Preprocessing QBF (pdf paper)
  Horst Samulowitz and Jessica Davies and Fahiem Bacchus
  published in CP 2006 (Twelfth International Conference on Principles and Practice of Constraint Programming), 2006.
  (a preliminary version of this paper also appears in NESCAI 2006 (North East Student Colloquium on Artificial Intelligence))
  
  
• Binary Clause Reasoning in QBF (pdf paper)
  Horst Samulowitz and Fahiem Bacchus
  published in SAT 2006 (Ninth International Conference on Theory and Applications of Satisfiability Testing), 2006.
  
  
• Using SAT in QBF (ps paper) (pdf paper)
  Horst Samulowitz and Fahiem Bacchus
  published in CP 2005 (Eleventh International Conference on Principles and Practice of Constraint Programming), 2005.
  (a shorter version of this paper also appears in NESCAI 2006 (North East Student Colloquium on Artificial Intelligence) (pdf paper), 2006)
  
  
• The Efficiency and Implementation of an Evaluation-Based Reasoning Procedure with Disjunctive Information in First-Order Knowledge Bases (Master Thesis)
  Horst Samulowitz
  Master Thesis, RWTH Aachen , 2003.
  
  
• Visualization of Eclipses and Planetary Conjunction Events: The Interplay between Model Coherence, Scaling and Animation (paper)
  Walter Oberschelp and Alexander Hornung and Horst Samulowitz
  in the Journal The Visual Computer , 2001.
  
  
• 3D-Visualization of Music
  Alexander Hornung and Horst Samulowitz
  in German Society for Computer Science (GI), Computer Science Days , 2001.
  
  
• Visualization of Eclipses and Planetary Conjunction Events: The Interplay between Model Coherence, Scaling and Animation
  Walter Oberschelp and Alexander Hornung and Horst Samulowitz
  in CGI 2000 (Computer Graphics International), 2000.