Abstract Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which limits their use in critical applications. In this work, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. We first describe a simple sequential algorithm and then present a fully distributed algorithm for proof composition, which is substantially more scalable and general than prior works. Our empirical evaluation with over 1500 solver threads shows that our distributed approach allows proof composition and checking within around 3 $$\times $$ × its own (highly competitive) solving time.

This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In this context, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of modular metatheory , by which we mean that proofs of relevant properties should be constructible by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called Sterling and a proof assistant called Extensibella and have used them to validate the examples that motivate the theoretical discussions.

Abstract Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which has limited their use in critical applications. In this paper, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. Our approach is more scalable and general than previous explorations for parallel clause-sharing solvers, allowing use on distributed solvers without shared memory. We propose a simple sequential algorithm as well as a fully distributed algorithm for proof composition. Our empirical evaluation shows that for large-scale distributed solvers (100 nodes of 16 cores each), our distributed approach allows reliable proof composition and checking with reasonable overhead. We analyze the overhead and discuss how and where future efforts may further improve performance.

We describe a monadification process for attribute grammars for more concisely written attribute equations, closer to the style of inference rules used in traditional typing and evaluation specifications. Inference rules specifying, for example, a typing relation typically consider only typable expressions, whereas well-defined attribute grammars explicitly determine attribute values for any term, including untypable ones. The monadification approach lets one represent, for example, types as monadic optional/maybe values, but write non-monadic equations over the value inside the monad that only specify the rules for a correct typing, leading to more concise specifications. The missing failure cases are handled by a rewriting that inserts monadic return, bind, and failure operations to produce a well-defined attribute grammar that handles untypable trees. Thus, one can think in terms of a type T and not the actual monadic type M(T). To formalize this notion, typing and evaluation relations are given for the original and rewritten equations. The rewriting is total, preserves types, and a correctness property relating values of original and rewritten equations is given. A prototype implementation illustrates the benefits with examples such as typing of the simply-typed lambda calculus with Booleans, evaluation of the same, and type inference in Caml Light.