SAT 2007 - Tenth International Conference on
Theory and Applications of Satisfiability Testing

May 28 - 31 2007, Lisbon, Portugal

Conference 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?
P. Manolios and D. Vroon
Efficient Circuit to CNF Conversion
C. Ansótegui Gil, M. L. Bonet, J. Levy and F. Manyà
Mapping CSP into Many-Valued SAT
G. Audemard and L. Sais
Circuit Based Encoding for CNF formulas
I. Lynce and J. Marques-Silva
Breaking Symmetries in SAT Matrix Models
J. Argelich and F. Manyà
Partial Max-SAT Solvers with Clause Learning
F. Heras, J. Larrosa and A. Oliveras
MiniMaxSat: a New Weighted Max-SAT Solver
M. Lukasiewycz, M. Glass, C. Haubelt and J. Teich
Solving Multi-Objective Pseudo-Boolean Problems
A. Kojevnikov
Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
M. Langlois, R. Sloan and G. Turan
Horn Upper Bounds and Renaming
S. Szeider
Matched Formulas and Backdoor Sets
C. Gomes, J. Hoffmann, A. Sabharwal and B. Selman
Short XORs for Model Counting: From Theory to Practice
S. Prestwich
Variable Dependency in Local Search: Prevention is Better than Cure
C.-M. Li, W. Wei and H. Zhang
Combining Adaptive Noise and Look-Ahead in Local Search for SAT
M. Heule and H. van Maaren
From Idempotent Generalized Boolean Assignments to Multi-Bit Search
D. Scheder and P. Zumstein
Satisfiability with Exponential Families
A. Hertel, P. Hertel and A. Urquhart
Formalizing Dangerous SAT Encodings
S. Porschen and E. Speckenmeyer
Algorithms for Variable-Weighted 2-SAT and Dual Problems
K. Makino, S. Tamaki and M. Yamamoto
On the Boolean Connectivity Problem for Horn Relations
T. Jussila, A. Biere, C. Sinz, D. Kroening and C. Wintersteiger
A First Step Towards a Unified Proof Checker for QBF
H. Samulowitz and F. Bacchus
Dynamically Partitioning for Solving QBF
M. Samer and S. Szeider
Backdoor Sets of Quantified Boolean Formulas
U. Bubeck and H. Kleine Buning
Bounded Universal Expansion for Preprocessing QBF
M. Heule and H. van Maaren
Effective Incorporation of Double Look-Ahead Procedures
N. Een, N. Sorensson and A. Mishchenko
Applying Logic Synthesis for Speeding Up SAT
A. Nadel, N. Dershowitz and Z. Hanna
Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver
K. Pipatsrisawat and A. Darwiche
A Lightweight Component Caching Scheme for Satisfiability Solvers
J. Buresh-Oppenheim and D. Mitchell
Minimum 2CNF Resolution Refutations in Polynomial Time
O. Kullmann
Polynomial Time SAT Decision for Complementation-invariant Clause-sets, and Sign-non-singular Matrices
A. Van Gelder
Verifying Propositional Unsatisfiability: Pitfalls to Avoid
A. Cimatti, A. Griggio and R. Sebastiani
A Simple and Flexible Way of Computing Small Unsatifiable Cores in SAT Modulo Theories
C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann and H. Zankl
SAT Solving for Termination Analysis with Polynomial Interpretations
S. Staber and R. Bloem
Fault Localization and Correction with QBF
F. Aloul and N. Kandasamy
Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach
D. De, A. Kumarasubramanian and R. Venkatesan
Inversion Attacks on Secure Hash Functions using SAT Solvers
QBF Evaluation
PB Evaluation
Max-SAT Evaluation
SAT Competition
Tobias Schubert, Multi-Threaded SAT Solving