Boolean SATisfiability problems
Course Description:
Boolean Satisfiability (SAT) is named after George Boole, whose 200th birthday we celebrate this year. The first step towards the use of SAT in real problems was probably taken in the 20's by Claude Shannon, one of the researchers who laid the foundations of AI. His master thesis connected Boolean logic with electrical applications. The next major step was performed by Stephen Cook in his seminal 70's paper on NP-completeness. SAT is now, in the 21st century, a widely used technology. Part of this success is explained by the efficiency of SAT solvers, namely Conflict Driven Clause Learning (CDCL) SAT solvers. In these lectures we will provide the basis for understanding SAT and its extensions (Maximum Satisfiability and Pseudo Boolean Optimization). Practical examples will be given for solving concrete problems with SAT, including all the required steps: encoding a problem into SAT, running a SAT solver and making use of the solution.Resume:
Inês Lynce is currently an associate Professor at IST - University of Lisbon and a senior researcher at INESC-ID. She is a well-established researcher in the area of Boolean constraint solving and optimization. Her main contributions refer to the development of search algorithms and the application of those algorithms to solve practical problems. Examples of these problems include software package upgreadability, biological networks, phylogenetic trees and crew scheduling. In 2006, she has pioneered, jointly with Joao Marques-Silva, the use of Boolean satisfiability in Bioinformatics. Since 2010 she is serving in the Editorial Board of the Journal of Artificial Intelligence Research (JAIR). She has been the workshop Chair of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14) and is recurrently member of the programme committees of the IJCAI, AAAI, ECAI, CP and SAT conferences.
Constraint Satisfaction Problems
Course Description:
Constraints can be a very natural way to solve a wide variety of problems, including real world problems like scheduling, puzzles like sudoku, and combinatorial problems in mathematics. The key feature is the availability in modern constraint solvers of a wide variety of semantically rich constraints, which can be reasoned with ("propagated") very efficiently. The fundamental principles of how constraint solvers reason will be covered, but the main focus will be on modelling of constraint problems with practical examples using the constraint modelling and solving tools SavileRow and Minion, both developed in St Andrews.Resume:
Ian Gent is Professor of Computer Science at the University of St Andrews, Scotland. Much of his research has been on Constraint Satisfaction, and has included topics such as symmetry in constraint problems, efficient propagation algorithms, the understanding of easy and hard problems in constraints, and modelling of constraint problems. He was Programme Chair of the major Constraint Programming conference, CP 2009 in Lisbon. More recently he founded recomputation.org, a website dedicated to reproducibility of experimental methods.
Answer Set Programming
Course Description:
This tutorial presents a practical introduction to Answer Set Programming (ASP), aiming at using ASP languages and systems for solving application problems. Starting from the essential formal foundations, it introduces ASP's modeling language and methodology, grounding and solving technology, and finally details control techniques needed for embedding ASP in complex software environments.Resume:
Torsten Schaub is University Professor at the University of Potsdam. His research interests range from the theoretic foundations to the practical implementation of reasoning from incomplete, inconsistent, and evolving information. His current research focus lies on Answer set programming and materializes at potassco.sourceforge.net, the home of the open source project Potassco bundling software for Answer Set Programming.
Knowledge Compilation
Course Description:
The course will include an introduction to the topic, as well as a presentation of the key notions of compilable problem and of knowledge compilation map. Some languages for the compilation of Boolean functions and of real-valued functions will be investigated. Recent developments, including the application of knowledge compilation techniques to product configuration, will be also overviewed.Resume:
Pierre Marquis is a Professor of Computer Science at Artois University. He does his research at CRIL. Pierre Marquis is a specialist of Knowledge Representation. One of his main topics for more than twenty years is Knowledge Compilation. Pierre Marquis authored or co-authored more than 30 papers on the subject in international journals and conferences.
SATisfiability Modulo Theory
Course Description:
This course will present a basic overview of SMT, mainly focusing on the DPLL(T) approach. We will review the most interesting theories that SMT solvers can deal with and will introduce the basic ingredients of a DPLL(T)-based SMT solver.Resume:
Albert Oliveras is associate professor at the Technical University of Caralonia (UPC). His research has been focused on developing theory, techniques and tools for SAT, SMT, decision procedures and program verification. He has co-authored more than 30 papers on these topics in international conferences and journals.
SAT for Data Mining
Course Description:
In this talk, we overview our contribution to data mining and more generally to the cross-fertilization between data mining and propositional satisfiability. We will focus on three contributions. First, we show how propositional satisfiability can be used to model and solve problems in data mining. As an illustration, we present a SAT-based declarative approach for enumerating top-k (closed, frequent) itemsets in transactional databases. Secondly, we show how symmetries widely investigated in Constraint Programming (CP) and Propositional Satisfiability (SAT) can be extended to deal with data mining problems. Finally, we discuss the potential contribution of data mining to propositional satisfiability. In this context, we present a first application of data mining to compress Boolean formulas conjunctive normal form.Resume:
Lakhdar Saïs is a Professor of Computer at Artois University - CRIL. His research focuses on search and representation problems in Artificial Intelligence. He is especially interested in propositional satisfiability, quantified boolean formula, constraint satisfaction and optimisation problems and data mining.
Weighted Constraint Satisfaction Problems
Course Description:
This course will first present Valued Constraint Satisfaction, a general framework for expressing finite-domain optimisation problems, before going on to discuss aspects such as modelling, search, problem transformations, tractable classes and applications. There will be an emphasis on the theory of valuation structures, soft consistency operations and tractable classes.Resume:
Martin Cooper holds a position of professor of Computer Science at Toulouse University. His research covers many aspects of constraint satisfaction, including tractable classes, reduction operations as well as applications in vision and planning. He has published over 30 journal papers on topics related to constraint satisfaction.
XCSP 3.0 input format
Course Description:
In this talk, we shall present the new format XCSP3 that allows us to build integrated representations of combinatorial constrained problems. This format is able to deal with mono/multi optimization, many types of variables, cost functions, reification, views, annotations, variable quantification, distributed, probabilistic and qualitative reasoning. Importantly, in this talk, XCSP3 will also serve as a pretext for presenting some facets of problem modelling and solving processes.Resume:
Christophe Lecoutre is a Professor of Computer Science at Artois University. He does his research at CRIL. Christophe Lecoutre is a specialist of Constraint Programming. Christophe Lecoutre authored a book about constraint networks and co-developed XCSP.
Evaluation & Competitions of Solvers
Course Description:
This course will focus on the difficulties met in assessing the performance of different solvers (software) on current computers. In a first part, the most relevant notions of computer architecture will be recalled (memory hierarchy, cores, SMP/NUMA architectures, ...). Then, some issues regarding the input format of the benchmarks and their selection will be presented. The experience gathered during the SAT, PB and CSP competitions will be shared in the third part. At last, different ranking methods used during the SAT competitions will be discussed.Resume:
Olivier Roussel is associate professor in computer science at University of Artois, France. He has organized many competitions (Pseudo-Boolean, SAT and CSP) and is the author of runsolver, a tool to control the resources used by a solver.
Daniel Le Berre is professor in computer science at University of Artois, France. He initiated the SAT competitive events in 2002, and took part of them in various roles (co-organizer, technical advisor) until 2011. As one of the authors of Sat4j, an open source Boolean satisfaction and optimization library, he also participated as competitor to many competitive events.
