Shared SAT Solvers and SAT Memory in Distributed Business Applications

TL;DR

This paper introduces a novel distributed architecture for SAT solvers with shared memory, enabling efficient SAT solving in business applications and simplifying integration from high-level languages.

Contribution

It presents a new shared SAT memory concept and architecture allowing multiple solvers to operate seamlessly across distributed systems.

Findings

Shared SAT memory enables concurrent access by multiple solvers.

Architecture simplifies SAT instance generation from high-level languages.

Demonstrated application on integer factorization problem.

Abstract

We propose a software architecture where SAT solvers act as a shared network resource for distributed business applications. There can be multiple parallel SAT solvers running either on dedicated hardware (a multi-processor system or a system with a specific GPU) or in the cloud. In order to avoid complex message passing between network nodes, we introduce a novel concept of the shared SAT memory, which can be accessed (in the read/write mode) from multiple different SAT solvers and modules implementing the business logic. As a result, our architecture allows for the easy generation, diversification, and solving of SAT instances from existing high-level programming languages without the need to think about the network. We demonstrate our architecture on the use case of transforming the integer factorization problem to SAT.