Robert Nieuwenhuis

SAT Modulo Theories: getting the best of SAT and global constraint filtering

Abstract: We first give an overview of Sat Modulo Theories (SMT), the DPLL(T) approach to SMT, and its implementation in our Barcelogic SMT tool.

Then we discuss current work on the development of SMT technology for hard combinatorial (optimization) problems outside the usual verification applications. The aim is to obtain the best of several worlds, combining the advantages inherited from SAT: efficiency, robustness and automation (no need for tuning) and CP features such as rich modeling languages, special-purpose filtering algorithms (for, e.g., planning, scheduling or timetabling constraints), and sophisticated optimization techniques. We give several examples and discuss the impact of aspects such as first-fail heuristics vs activity-based ones, realistic structured problems vs random or handcrafted ones, and lemma learning.

Edward Tsang

Click here for abstract

Moshe Y. Vardi

Constraints, Graphs, Algebra, Logic, and Complexity

Abstract: A large class of problems in AI and other areas of computer science can be viewed as constraint-satisfaction problems. This includes problems in database query optimization, machine vision, belief maintenance, scheduling, temporal reasoning, type reconstruction, graph theory, and satisfiability. All of these problems can be recast as questions regarding the existence of homomorphisms between two directed graphs. It is well-known that the constraint-satisfaction problem is NP-complete. This motivated an extensive research program into identify tractable cases of constraint satisfaction.

This research proceeds along two major lines. The first line of research focuses on non-uniform constraint satisfaction, where the target graph is fixed. The goal is to identify those target graphs that give rise to a tractable constraint-satisfaction problem. The second line of research focuses on identifying large classes of source graphs for which constraint-satisfaction is tractable. We show in this talk how tools from graph theory, universal algebra, logic, and complexity theory, shed light on the tractability of constraint satisfaction.