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.

翻译：我们提出一种软件架构，其中SAT求解器作为分布式业务应用的共享网络资源运行。该架构支持多个并行SAT求解器在专用硬件（多处理器系统或配备特定GPU的系统）或云端执行。为避免网络节点间复杂的消息传递，我们引入共享SAT内存这一创新概念，该内存可从多个不同SAT求解器及实现业务逻辑的模块以读写模式访问。由此，该架构使开发者能够从现有高级编程语言中便捷地生成、多样化并求解SAT实例，而无需考虑网络细节。我们通过将整数分解问题转化为SAT实例的用例，对该架构进行了验证。