PaInleSS (Parallel Instantiable SAT Solver) is a framework written in C++ and developed by the Automata and Applications team, the MoVe team at LIP6, and the DELYS team at LIP6/Inria. It simplifies the implementation and evaluation of new parallel SAT solvers for multicore environments. The components of PaInleSS can be instantiated independently to produce a new complete solver. The guiding principle is to separate the technical components dedicated to a specific aspect of concurrent programming from the components implementing heuristics and optimizations integrated into a parallel SAT solver. As a result, the developer of a parallel solver can focus efforts on functional aspects such as parallelization and sharing strategies, while delegating implementation concerns (e.g., mechanisms for protecting concurrent data access) to the framework.

Three main components emerge in the design of parallel SAT solvers: sequential engines, parallelization, and sharing.

• The central element is a sequential SAT solver (called the sequential engine). This can be any state-of-the-art CDCL solver. Technically, these engines are exploited via a generic interface providing the basic capabilities of sequential solvers: solving, interruptions, clause addition, etc. Thus, to instantiate PaInleSS with a particular solver, one only needs to implement an interface with this engine.

• To build a parallel solver using the aforementioned engines, it is necessary to define and implement a parallelization strategy. In PaInleSS, a strategy is represented by a tree structure of arbitrary depth. The internal nodes of the tree represent parallelization strategies, and the leaves are base engines. Therefore, to develop a custom parallelization strategy, the user must combine one or more existing strategies to construct a tree structure.

• In parallel SAT solving, the exchange of learned clauses requires particular attention. Beyond the theoretical aspects, a poor implementation of an otherwise good sharing strategy can dramatically impact solver efficiency. In PaInleSS, solvers can export (import) clauses to (from) others during the solving process. Technically, this is done using lock-free queues. Thus, the only part requiring a custom implementation is the exchange phase, which is defined by the user.