Conference Programme

The locations are as follows:

• All talks take place in the "Faraday Lecture Theatre" in the Faraday building.
• The reception, registration and all breaks take place in "Seminar Room 2" in Fulton House.
• Breakfasts, lunchs and normal dinners take place in the refactory in Fulton House.

Monday

• 16:00 - 16:30 Reception

• 16:00 - 18:30 Registration

• 18:30 Dinner

Tuesday

• 7:30 - 9:00 Breakfast

• 9:00 - 9:30 Opening, introduction

• Chair: John Franco

  9:30 - 9:50

  The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. Stefan Szeider.

  9:50 - 10:10

  Does Advice Help to Prove Propositional Tautologies? Olaf Beyersdorff, Sebastian Müller.

  10:10 - 10:30

  A Theoretical Analysis of Search in GSAT. Evgeny Skvortsov.

• 10:30 - 11:00 Interval

• Chair: Armin Biere

  11:00 - 11:25

  Efficiently Calculating Tree Measures Using SAT. Maria Luísa Bonet, Katherine St. John.

  11:25 - 11:50

  Finding Lean Induced Cycles in Binary Hypercubes. Yury Chebiryak, Thomas Wahl, Daniel Kröning, Leopold Haller.

  11:50 - 12:10

  Finding Efficient Circuits Using SAT-solvers. Arist Kojevnikov, Alexander Kulikov, Grigory Yaroslavtsev.

  12:10 - 12:30

  An exponential lower bound for width-restricted clause learning. Jan Johannsen.

• 12:30 - 12:45 Conference Photo

• 12:45 - 14:00 Lunch

• Chair: Stefan Szeider

  14:00 - 14:25

  The Complexity of Reasoning for Fragments of Default Logic Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer.

  14:25 - 14:50

  On Some Aspects of Mixed Horn Formulas. Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer.

  14:50 - 15:15

  Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. Albert Atserias, Johannes Fichte, Marc Thurley.

  15:15 - 15:30

  Backdoors in the Context of Learning. Bistra Dilkina, Carla Gomes, Ashish Sabharwal.

• 15:30 - 16:00 Interval

• Chair: Ashish Sabharwal

  16:00 - 16:25

  Boundary Points and Resolution. Eugene Goldberg.

  16:25 - 16:50

  Dynamic Symmetry Breaking by Simulating Zykov Contraction. Bas Schaafsma, Marijn Heule, Hans van Maaren.

  16:50 - 17:15

  New Encodings of Pseudo-Boolean Constraints into CNF. Olivier Bailleux, Yacine Boufkhad, Olivier Roussel.

  17:15 - 17:40

  Efficient Term-ITE Conversion for Satisfiability Modulo Theories Hyondeuk Kim, Fabio Somenzi, HoonSang Jin.

  17:40 - 18:00

  Variable Influences in Conjunctive Normal Forms. Patrick Traxler.

• 18:30 Dinner

• 19:30 - 21:00 SAT business meeting ( Robert Recorde Room)

Wednesday

• 7:30 - 9:00 Breakfast

• Chair: Daniel Le Berre

  9:00 - 9:25

  Cardinality Networks and their Applications. Roberto Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell.

  9:25 - 9:50

  Sequential Encodings from Max-CSP into Partial Max-SAT. Josep Argelich, Alba Cabiscol, Inês Lynce, Felip Manyà.

  9:50 - 10:15

  On-The-Fly Clause Improvement. Hyojung Han, Fabio Somenzi.

  10:15 - 10:30

  Problem-Sensitive Restart Heuristics for the DPLL Procedure. Carsten Sinz, Markus Iser.

• 10:30 - 11:00 Interval and Poster Contact Time

• Chair: Roberto Sebastiani

  11:00 - 12:00 Invited Talk

  SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms Robert Nieuwenhuis

  12:00 - 12:15

  Minimizing Learned Clauses. Niklas Sörensson, Armin Biere.

  12:15 - 12:30

  Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. Allen Van Gelder.

• 12:30 - 14:00 Lunch

• Chair: Marijn Heule

  14:00 - 14:25

  Extending SAT solvers to cryptographic problems. Mate Soos, Karsten Nohl, Claude Castelluccia.

  14:25 - 14:50

  A novel approach to combine a SLS- and a DPLL-solver for the satisfiability problem. Adrian Balint, Michael Henn, Oliver Gableske.

  14:50 - 15:15

  Building a Hybrid SAT Solver via Conflict-driven, Look-ahead and XOR Reasoning Techniques. Jingchao Chen.

  15:15 - 15:30

  Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability. Zbigniew Stachniak, Anton Belov.

• 15:30 - 16:00 Interval

• Chair: Fahiem Bacchus

  16:00 - 16:25

  Restart Strategy Selection using Machine Learning Techniques. Shai Haim, Toby Walsh.

  16:25 - 16:50

  Instance-Based Selection of Policies for SAT Solvers. Mladen Nikolić, Filip Marić, Predrag Janičić.

  16:50 - 17:15

  VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search. Eric Hsu, Sheila McIlraith.

  17:15 - 17:40

  (1,2)-QSAT: a good candidate for understanding phase transition mechanisms. Nadia Creignou, Hervé Daudé, Uwe Egly, Raphaël Rossignol.

  17:40 - 17:55

  Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits. Hans Kleine Büning, Xishun Zhao, Uwe Bubeck.

• Chair: Faron Moller

  18:30 - 19:30 Invited Talk

  SAT in the Railway Industry Simon Chadwick, Director of Research, Westinghouse Rail Systems Limited, Chippenham.

• 19:30 - 20:00 Reception

• 20:00 Informal Banquet

Thursday

• 7:30 - 9:00 Breakfast

• Chair: Enrico Giunchiglia

  9:00 - 9:25

  Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. Knot Pipatsrisawat, Adnan Darwiche.

  9:25 - 9:50

  A Compact Representation for Syntactic Dependencies in QBFs. Florian Lonsing, Armin Biere.

  9:50 - 10:15

  Beyond CNF: a Circuit-Based QBF Solver. Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus.

  10:15 - 10:30

  Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation? Timo Berthold, Stefan Heinz, Marc E. Pfetsch.

• 10:30 - 11:00 Interval and Poster Contact Time

• Chair: Hans Kleine Büning

  11:00 - 12:00 Invited Talk

  Symbolic Techniques in Propositional Satisfiability Solving Moshe Vardi

  12:00 - 12:15

  Encoding Treewidth into SAT. Marko Samer, Helmut Veith.

  12:15 - 12:30

  Solving SAT for CNF formulas with a one-sided variable occurrence restriction. Daniel Johannsen, Igor Razgon, Magnus Wahlström.

• 12:50 Departure for Gower Tour

• 18:30 Departure for National Waterfront Museum

• 20:00 - 22:30 Banquet (in the Museum)

Friday

• 7:30 - 9:00 Breakfast

• Chair: Carsten Sinz

  9:00 - 9:25

  Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell.

  9:25 - 9:50

  Exploiting Cycle Structures in Max-SAT. Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou, Jordi Planes.

  9:50 - 10:15

  Algorithms for Weighted Boolean Optimization. Vasco Manquinho, Joao Marques-Silva, Jordi Planes.

  10:15 - 10:30

  Relaxed DPLL Search for MaxSAT. Lukas Kroc, Ashish Sabharwal, Bart Selman.

• 10:30 - 11:00 Interval

• Chair: Sean Weaver

  11:00 - 11:25

  PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia.

  11:25 - 11:50

  c-sat: A Parallel SAT Solver for Clusters. Kei Ohmura, Kazunori Ueda.

  11:50 - 12:15

  Generalizing Core-Guided Max-SAT. Mark Liffiton, Karem Sakallah.

  12:15 - 12:40

  A Weighted Partial MaxSAT Solver Based on Satisfiability Testing. Carlos Ansótegui, María Luisa Bonet, Jordi Levy.

• 12:40 - 14:00 Lunch

• 14:00 - 15:30 : Competition session I

• 15:30 - 16:00 Interval

• 16:00 - 17:30 : Competition session II and Panel

• 17:30 - 18:00 Conclusion

• 18:30 Dinner

Saturday

• 7:30 - 9:00 Breakfast

• 10:00 Checkout

---

Last modified: Sat Sep 19 19:05:15 BST 2009