ABSTRACT. This talk explains how to efficiently translate the domain problem into a
set of clauses, the input taken by the SAT solvers. The presentation will
emphasize the importance of the encoding and present some preprocessing
techniques available in the SAT solver Lingeling.

ABSTRACT. Satisfiability (SAT) solvers have become powerful tools to solve a wide range of applications. In case SAT problems are satisfiable, it is easy to validate a witness. However, if SAT problems have no solutions, a proof of unsatisfiability is required to validate that result. Apart from validation, proofs of unsatisfiability are useful in several applications, such as interpolation and extracting a minimal unsatisfiable set and in tools that use SAT solvers such as theorem provers. This talk will present the recent advances in checking proofs of unsatisfiability: both the concepts behind proofs and the state-of-the-art tool, DRAT-trim, to validated them will be presented.

ABSTRACT. SAT solvers are used in a growing range of practical applications.
In many settings, SAT solvers are used iteratively to solve problems
that lie beyond the class of NP decision problems, i.e. which are
believed to be harder than SAT. This talk surveys recent work on
problem solving with SAT engines by analyzing a number of case
studies. Concretely, this talk overviews approaches for solving
Quantified Boolean Formulae (QBF) with abstraction refinement, for
solving Maximum Satisfiability (MaxSAT) using iterative unsatisfiable
subformula identification, and for finding minimal explanations of
inconsistency.

ABSTRACT. Solvers are usually parameterized, and different settings can lead to quite different behavior on different instances in practice. As such, a tedious task for the user is to optimize the settings of the solver for his particular needs. Experts (aka solvers designers) have usually a good intuition about the solvers internals to provide settings good enough for a class of problems they are familiar with. This task is much more challenging for simple users of the solvers or experts on arbitrary problems. Fortunately, there exists now software to help experts and users to automate this task. Marius Lindauer will introduce SMAC, a state-of-the-art tool for automatic algorithm configuration.