ABSTRACT. Given a propositional formula F in Conjunctive Normal Form (CNF), a SAT solver decides whether it is satisfiable or not. It is often required to find a solution to a satisfiable CNF formula F, which optimizes a given Pseudo-Boolean objectivefunction Ψ, that is, to extend SAT to optimization.

MaxSAT is a widely used extension of SAT to optimization. A MaxSAT solver can be applied to optimize a Pseudo-Boolean objective function Ψ, given a CNF formula F, whenever Ψ is a linear function.

MaxSAT has a diverse plethora of applications, including applications in computer-aided design, artificial intelligence, planning, scheduling and bioinformatics. A variety of approaches to MaxSAT have been developed over the last two decades. In this tutorial, we focus on anytime MaxSAT algorithms, where an anytime algorithm is expected to find better and better solutions,the longer it keeps running. The anytime property is crucial in industrial applications, since it allows the user to: 1) get an approximate solution even for very difficult instances, and 2) trade quality for performance by regulating the timeout.

Anytime MaxSAT solvers have been evaluated at yearly MaxSAT Evaluations since 2011 in the so-called incomplete tracks. We trace the evolvement of anytime MaxSAT algorithms over the last decade and lay out the algorithms, applied by the winners of MaxSAT Evaluation 2020.

Furthermore, we touch upon anytime algorithms for optimization problems beyond MaxSAT, such as bit-vector optimization and the problem of optimizing an arbitrary not-necessarily-linear function, given a CNF formula. Finally, we discuss challenges and future work.

ABSTRACT. Computational modeling is now used effectively to complement experimental work in biology, allowing to identify gaps in the understanding of the biological systems studied, and to predict system behavior based on a mechanistic models. We provide an overview of several areas in biology for which formal verification has been successfully used to advance the state-of-the-art in biological modeling, highlighting examples from both natural and engineered biological systems. In natural biological systems the main goal is to understand how a system works and predict its behavior, whereas for engineered biological systems the main goal is to engineer biological systems for new purposes, e.g. for building biology-based computational devices. We compare between the challenges in applying formal verification in biology and the application to traditional hardware and software domains and outline future research directions and opportunities for formal verification experts to contribute to the field.

ABSTRACT. In SMT bit-vectors and thus word-level reasoning is common and widely used in industry. However, it took until 2019 that the hardware model checking competition used word-level benchmarks. Reasoning on the word-level opens up many possibilities for simplification and more powerful reasoning. In SMT we do see advantages due to operating on the word-level, even though, ultimately, bit-blasting and thus transforming the word-level problem into SAT is still the dominant and most important technique. For word-level model checking the situation is different. As the hardware model checking competition in 2019 has shown bit-level solvers are far superior (after bit-blasting the model through an SMT solver though). On the other hand word-level model checking shines for problems with memory modeled with arrays. In this tutorial we revisit the problem of word level model checking, also from a theoretical perspective, then give and overview on classical and more recent approaches for word-level model checking and then discuss challenges and future work.