| |
Topics related to Knowledge Representation and Constraint Satisfaction.
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 #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 search based algorithms.
|
Publications |
|
|
|
|
|
-
Learning to Solve QBF
(pdf paper)
Horst Samulowitz and Roland Memisevic
To appear in AAAI 2007 (Twenty-Second Conference on Artificial Intelligence), 2007.
-
Solution Backjumping for #SAT (short paper)
Jessica Davies and Eric Hsu and Horst Samulowitz
To appear in NESCAI 2007 (North East Student Colloquium on Artificial Intelligence), 2007
-
Dynamically Partitioning for Solving QBF
(pdf paper)
Horst Samulowitz and Fahiem Bacchus
To appear 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
to be 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.
|
|
Software
Links |
|
|
|
|
|
- Software of the QBF solver SQBF (3rd Place QBF Competition 2006).
- Software of the QBF solver 2clsQ (1st Place QBF Competition 2006).
- Software of the Preprocessor Prequel for QBFs.
All Software is available here .
- Also see the results of the first QBF competition 2006
-
Here is a very simple script that can be used to run first the preprocessor PreQuel, second time-limited Quantor, and third 2clsQ as a batch job.
|
|
|
CV / Resume |
|
|
CV
(pdf),
(ps)
(last updated January 2007)
Resume
(pdf)
(last updated January 2007)
|
|
|
Awards |
|
|
|
|
|
-
Winner of the QBF Competition 2006 (Official Competition Homepage)
1st, 2nd and 3rd place on industrial benchmarks
2nd place on random benchmarks
|
| |
 |
|
|
|
Contact Information |
|
Office Location:
|
Pratt Building,
6 King's College Road, University of Toronto
|
Mailing Adress:
|
University of Toronto,
Dept. of Computer Science,
Pratt Building, Room 283,
6 King's College Road,
Toronto, ON M5S 3H5,
CANADA
|
E-mail address:
|
horst[at]cs[dot]toronto[dot]edu
|
|
| |
|
|
|
|
Links |
|
|
DCS Webmail access
|
|
AppGate MindTerm DCS
|
|
