Building high-performance SAT solvers is an art that requires deep expert knowledge and access to ideas that have been developed within small communities, mainly in Europe and a few places in the United States and Japan, Singapore, Korea, Taiwan and China. By organizing a seminar at Shonan, a goal is to bring experts from development of SAT engines to Japan to interact with communities that have invested in SAT search technologies.

In recent years, SAT solvers have been used to solve long-standing open problems in mathematics, including the Pythagoreans triples problem, Erdos discrepancy problem, Keller's conjecture and the chromatic number of the plane. Some mathematicians argue that these solutions don't contribute to understanding. However, the solutions and proofs produced by SAT solvers reveal interesting patterns and can provide mathematical insights and result in artistic images. Also, there has been much work on using solutions and proofs produced by SAT solvers for various applications in computer science, such as using interpolants computed from the unsatisfiability proofs produced by SAT solvers for program veri cation and synthesis. A goal of the seminar at Shonan is to explore which useful information can be extracted from SAT solutions and proofs from various applications.

Tools built around SAT solvers abound and the seminar includes several users of SAT and SMT technologies. Japan has a strong community in term rewriting where SAT solvers have been used for dependency pair constraints and solving other constraints derived from analysis of rewriting systems. A long-running theme in program analysis is to establish program termination arguments. They can be obtained automatically by synthesizing so-called transition invariants. These are well-founded measures that decrease with every step of a program. These measures can often be synthesized as satisfiable solutions to SAT (and SMT) problems. In other activities, programming language researchers at Todai, Waseda and Tsukuba seek solutions to fixed-point constraints that use SAT and SMT solvers to discharge subgoals. Researchers in Osaka have developed novel algorithms for combinatorial optimization using SAT and others in Kyoto invented widely used novel data-structures for representing sets of solutions to SAT formulas. Finally, researchers at Tsukuba have harnessed FPGAs to accelerate local search.

Active areas pursued by the international community of SAT researchers include, to mention a few, using lookahead search techniques to speed up parallel SAT solving; using machine learning to con gure and tune SAT solvers; integrate specialized solvers for Boolean functions, such as pseudo-Boolean inequalities and parity constraints; new inference mechanisms that extends the power of SAT solvers beyond the limitations of resolution. The seminar would bring experts in these domains to Shonan to share their insights and inspire and strengthen research in SAT solving.

The seminar will have two main sections around the Art of SAT:

1. Art of SAT: Participants will present their newest  ndings in building SAT solvers.
2. Art from SAT: Participants present novel uses of SAT solvers.

The seminar will give the participants an opportunity to share their latest work around SAT solving in an environment that allows a high degree of interaction. We will ask the participants to share challenge problems, or puzzles, that have arisen from their research. These problems will be revisited during the seminar and in breakout sessions where participants can collaborate in smaller groups. The participants can discuss what ideas were developed during the seminar in the regular sessions.

Sunday

Arrival and social.

Monday

Morning: Participants introduce themselves, introduction of challenge problems, 2 tutorials.

Afternoon 1: Topic session on new methods for SAT search (part I).

Afternoon 2: Topic session on applications of SAT.

Evening: Demos and social interaction.

Tuesday

Morning 1: Topic session on building SAT services on top of SAT solvers.

Morning 2: Topic session on harnessing SAT using modern hardware resources.

Afternoon 1: Topic session on solution strategies for challenge problems.

Afternoon 2: Topic session on new methods for SAT search (part II). Breakout session for collaborations.

Evening: Social interaction.

Wednesday

Morning 1: Topic session on certifying SAT.

Morning 2: Breakout session for collaborations.

Afternoon and evening: Excursion and banquet.

Thursday

Morning: 5 contributed talks. Discussions on the challenge problems.

Afternoon: departure.