Shared SAT Solvers and SAT Memory in Distributed Business Applications
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.
Cite
@article{arxiv.2302.00635,
title = {Shared SAT Solvers and SAT Memory in Distributed Business Applications},
author = {Sergejs Kozlovičs},
journal= {arXiv preprint arXiv:2302.00635},
year = {2023}
}
Comments
This preprint has not undergone peer review or any post-submission improvements or corrections. The Version of Record of this contribution is published in CCIS vol. 1598, "Digital Business and Intelligent Systems: 15th International Baltic Conference, Baltic DB&IS 2022, Riga, Latvia, July 4-6, 2022, Proceedings", pp.201-216, and is available online at https://doi.org/10.1007/978-3-031-09850-5_14