The Coq mailing list

[Joao Marques-Silva <jpms AT ecs.soton.ac.uk>]

      Apologies if you receive multiple copies of this announcement.


                               SAT 2007

 International Conference on Theory and Applications of Satisfiability Testing

                          http://sat07.soton.ac.uk/

                           CALL FOR PARTICIPATION

                      May 28-31, 2007, Lisbon, Portugal


                 -------------------------------------------
                 Early Registration Deadline:  April 9, 2007
                 -------------------------------------------

The International Conference on Theory and Applications of Satisfiability
Testing is the primary annual meeting for researchers studying the
propositional satisfiability problem (SAT). The SAT conference also hosts
a number of competitions and evaluations, including the SAT competition,
the QBF competition, the Pseudo-Boolean evaluation, and the MAX-SAT
evaluation. 


Invited Talks
--------------------------------------------------------------------------------
Martin Davis, SAT: Past and future

Andrei Voronkov, Encodings of Problems in Effectively Propositional Logic 

Armin Biere, A Short History of SAT Solver Technology and What is Next?


Competitions and Evaluations
--------------------------------------------------------------------------------
SAT Competition

QBF Competition

PB Evaluation

MAX-SAT Evaluation


SAT 2007 Program
--------------------------------------------------------------------------------

Sunday, May 27

19:00-21:00  SAT Reception


Monday, May 28

09:00-09:30  Introduction and Welcome

09:30-10:30  Session 1: Encodings

09:30   P. Manolios and D. Vroon
        Efficient Circuit to CNF Conversion
09:45   C. Ansotegui Gil, M. L. Bonet, J. Levy and F. Manya
        Mapping CSP into Many-Valued SAT
10:00   G. Audemard and L. Sais
        Circuit Based Encoding for CNF formulas
10:15   I. Lynce and J. Marques-Silva
        Breaking Symmetries in SAT Matrix Models

10:30-11:00  Coffee break

11:00-12:30  Session 2: Max-SAT and Pseudo-Boolean

11:00   J. Argelich and F. Manya
        Partial Max-SAT Solvers with Clause Learning
11:30   F. Heras, J. Larrosa and A. Oliveras
        MiniMaxSat: a New Weighted Max-SAT Solver
12:00   M. Lukasiewycz, M. Glass, C. Haubelt and J. Teich
        Solving Multi-Objective Pseudo-Boolean Problems

12:30-14:00  Lunch break

14:00-15:30  Session 3: Structure I

14:00   A. Kojevnikov
        Improved Lower Bounds for Tree-Like Resolution over Linear 
Inequalities
14:30   M. Langlois, R. Sloan and G. Turan
        Horn Upper Bounds and Renaming
15:00   S. Szeider
        Matched Formulas and Backdoor Sets
15:15   C. Gomes, J. Hoffmann, A. Sabharwal and B. Selman
        Short XORs for Model Counting: From Theory to Practice

15:30-16:00  Coffee break

16:00-17:30  Session 4: Local Search

16:00   S. Prestwich
        Variable Dependency in Local Search: Prevention is Better than Cure
16:30   C.-M. Li, W. Wei and H. Zhang
        Combining Adaptive Noise and Look-Ahead in Local Search for SAT
17:00   M. Heule and H. van Maaren
        From Idempotent Generalized Boolean Assignments to Multi-Bit Search


Tuesday, May 29

09:00-10:00  Invited Talk:
             Martin Davis, SAT: Past and future

10:00-10:30  Coffee break

10:30-12:30  Session 5: Structure II

10:30   D. Scheder and P. Zumstein
        Satisfiability with Exponential Families
11:00   A. Hertel, P. Hertel and A. Urquhart
        Formalizing Dangerous SAT Encodings
11:30   S. Porschen and E. Speckenmeyer
        Algorithms for Variable-Weighted 2-SAT and Dual Problems
12:00   K. Makino, S. Tamaki and M. Yamamoto
        On the Boolean Connectivity Problem for Horn Relations

12:30-14:00  Lunch break

14:00-18:00  Social Programme


Wednesday, May 30

09:00-10:00  Invited Talk
             Andrei Voronkov, Encodings of Problems in Effectively
                              Propositional Logic 

10:00-10:30  Coffee break

10:30-12:30  Session 6: QBF

10:30   T. Jussila, A. Biere, C. Sinz, D. Kroening and C. Wintersteiger
        A First Step Towards a Unified Proof Checker for QBF
11:00   H. Samulowitz and F. Bacchus
        Dynamically Partitioning for Solving QBF
11:30   M. Samer and S. Szeider
        Backdoor Sets of Quantified Boolean Formulas
12:00   U. Bubeck and H. Kleine Buning
        Bounded Universal Expansion for Preprocessing QBF

12:30-14:00  Lunch break

14:00-15:30  Session 7: Complete Algorithms

14:00   M. Heule and H. van Maaren
        Effective Incorporation of Double Look-Ahead Procedures
14:30   N. Een, N. Sorensson and A. Mishchenko
        Applying Logic Synthesis for Speeding Up SAT
15:00   A. Nadel, N. Dershowitz and Z. Hanna
        Towards a Better Understanding of the Functionality of a
        Conflict-Driven SAT Solver
15:15   K. Pipatsrisawat and A. Darwiche
        A Lightweight Component Caching Scheme for Satisfiability Solvers

15:30-16:00  Coffee break

16:00-17:30  Session 8: Proofs and Cores

16:00   J. Buresh-Oppenheim and D. Mitchell
        Minimum 2CNF Resolution Refutations in Polynomial Time
16:30   O. Kullmann
        Polynomial Time SAT Decision for Complementation-invariant
        Clause-sets, and Sign-non-singular Matrices
17:00   A. Van Gelder
        Verifying Propositional Unsatisfiability: Pitfalls to Avoid
17:15   A. Cimatti, A. Griggio and R. Sebastiani
        A Simple and Flexible Way of Computing Small Unsatifiable
        Cores in SAT Modulo Theories

19:30-22:30  Social Programme: Conference Banquet


Thursday, May 31

09:00-10:30  Session 9: Applications

09:00   C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp,
        R. Thiemann and H. Zankl
        SAT Solving for Termination Analysis with Polynomial
        Interpretations
09:30   S. Staber and R. Bloem
        Fault Localization and Correction with QBF
10:00   F. Aloul and N. Kandasamy
        Sensor Deployment for Failure Diagnosis in Networked Aerial
        Robots: A Satisfiability-Based Approach
10:15   D. De, A. Kumarasubramanian and R. Venkatesan
        Inversion Attacks on Secure Hash Functions using SAT Solvers

10:30-11:00  Coffee break and Poster session

11:00-12:30  Session 10: Competitions and Evaluations

11:00   QBF Evaluation
11:20   PB Evaluation
11:40   Max-SAT Evaluation
12:00   SAT Competition

12:30-14:00  Lunch break

14:00-16:00  Special Session on Modern SAT Solving

14:00   Invited Talk
        Armin Biere, A Short History of SAT Solver Technology
                     and What is Next?
15:00   Highlights from the SAT Competition

16:00-17:00  Coffee break and Poster session

17:00  End of Conference


Organization
--------------------------------------------------------------------------------
Chairs:                 
Joao Marques-Silva, University of Southampton, UK
Karem A. Sakallah, University of Michigan, USA
                        
Local Arrangements:     
Ines Lynce, Technical University of Lisbon, Portugal

Program Committee:
Fahiem Bacchus, University of Toronto, Canada
Paul Beame, University of Washington, USA
Armin Biere, Johannes Kepler University, Austria
Adnan Darwiche, UCLA, USA
Leonardo de Moura, Microsoft Research, USA
Niklas Een, Cadence Design Systems, USA
John Franco, University of Cincinnati, USA
Ian Gent, University of St. Andrews, UK
Enrico Giunchiglia, Universita di Genova, Italy
Carla Gomes, Cornell University, USA
Aarti Gupta, NEC Research Labs, USA
Ziyad Hanna, Intel Corp., USA
Edward Hirsch, Steklov Inst. of Mathematics, Russia
Joonyoung Kim, Intel Corp., USA
Hans Kleine-Buning, Univ. Paderborn, Germany
James Kukula, Synopsys ATG, USA
Oliver Kullmann, University of Wales Swansea, UK
Daniel Le Berre, Universite d'Artois, France
Chu-Min Li, Universite de Picardie, France
Ines Lynce, Technical University of Lisbon, Portugal
Panagiotis Manolios, Georgia Institute of Technology, USA
Vasco Manquinho, Technical University of Lisbon, Portugal
Slawomir Pilarski, Magma DA, USA
Steve Prestwich, University College Cork, Ireland
Roberto Sebastiani, Universita di Trento, Italy
Hossein Sheini, CMU, USA
Laurent Simon, Universite Paris Sud, France
Ewald Speckenmeyer, Universitat Koln, Germany
Ofer Strichman, Technion, Israel
Stefan Szeider, Durham University, UK
Armando Tacchella, Universita di Genova, Italy
Allen Van Gelder, UC Santa Cruz, USA
Hans van Maaren, Technische Universiteit Delft, Netherlands
Toby Walsh, National ICT, Australia
Lintao Zhang, Microsoft Research, USA
--------------------------------------------------------------------------------