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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Given a Boolean formula F, determine whether there exists an assignment for all Boolean variables used in F such that F evaluates to true.
- 2.
For SAT, the proof could consist of assignments for the variables and a polynomial algorithm for evaluating the SAT formula.
- 3.
Institute of Mathematics and Computer Science, University of Latvia.
- 4.
Such as Nvidia T4 16 GB GPU (used in our experiments).
- 5.
MapleSAT has multiple configurations. It is based on MiniSAT [10]; see https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/maplesat.
- 6.
- 7.
If interface I is a set of web methods \(m_1, m_2, \dots ,\) and the object o is included in web memory classes \(C_1, C_2, \dots \), then o implements I, iff \(\forall m_i\exists C_j:\) ClassName(\(C_j\)).methodName(\(m_i\)) \(\in \) Code Space.
- 8.
This implies that web I/O devices must be implemented in a thread-safe way.
- 9.
In this paper, we cover CNF only.
- 10.
- 11.
Technically, in order to avoid copying of clauses, the common part with the original SAT memory is factored out and stored only once.
- 12.
Direct memory access.
- 13.
The extension of the HTTP protocol for highly-efficient bi-directional communication via the network.
- 14.
For the sake of clarity, we omitted the web kernel and some steps of Fig. 2.
- 15.
The Davis–Putnam–Logemann–Loveland algorithm.
- 16.
Conflict-driven clause-learning.
- 17.
Variable State Independent Decaying Sum.
- 18.
In 2022, it is available at https://github.com/joebebel/toughsat.git; older references point to https://toughsat.appspot.com/, which is no more available.
References
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley Series in Computer Science and Information Processing. Addison-Wesley, Reading (1974)
Andrews, M., Whittaker, J.A.: How to Break Web Software: Functional and Security Testing of Web Applications and Web Services. Addison-Wesley Professional, Boston (2006)
Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(01), 1840001 (2018)
Balyo, T., Sanders, P., Sinz, C.: HordeSat: a massively parallel portfolio SAT solver, May 2015. https://doi.org/10.1007/978-3-319-24318-4_12
Bebel, J.: Harder SAT Instances from Factoring with Karatsuba and Espresso. In: Proceedings of SAT Race 2019. University of Helsinki (2019)
Biere, A., Heule, M., Maaren, H.V. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 336, 2nd edn. IOS Press, Amsterdam; Washington, DC (2021). oCLC: on1250382566
Boulanger, J.L. (ed.): Formal Methods Applied to Complex Systems: Implementation of the B Method. Computer Engineering Series, ISTE; Wiley, London: Hoboken, New Jersey (2014)
Braunstein, A., Mezard, M., Zecchina, R.: Survey propagation: an algorithm for satisfiability. Random Struct. Algorithms 27, 201–226 (2005)
Eggersglüss, S., Eggersglüß, S., Drechsler, R.: High Quality Test Pattern Generation and Boolean Satisfiability. Springer, New York (2012). https://doi.org/10.1007/978-1-4419-9976-4
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Folino, G., Pizzuti, C., Spezzano, G.: Parallel hybrid method for SAT that couples genetic algorithms and local search. IEEE Trans. Evol. Comput. 5(4), 323–334 (2001)
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6, 245–262 (2009)
Huang, J.: Universal booleanization of constraint models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144–158. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85958-1_10
Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, vol. 2, 3rd edn. Addison-Wesley, Reading (1997)
Kozlovičs, S.: The web computer and its operating system: a new approach for creating web applications. In: Proceedings of the 15th International Conference on Web Information Systems and Technologies (WEBIST 2019), Vienna, Austria, pp. 46–57. SCITEPRESS (2019)
Kozlovičs, S.: webAppOS: creating the illusion of a single computer for web application developers. In: Bozzon, A., Domínguez Mayo, F.J., Filipe, J. (eds.) WEBIST 2019. LNBIP, vol. 399, pp. 1–21. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61750-9_1
Li, K., Hudak, P.: Memory coherence in shared virtual memory systems. ACM Trans. Comput. Syst. 7(4), 321–359 (1989)
Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (IEEE cat. No. 01CH37232), pp. 530–535 (2001)
Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74970-7_38
Ozolins, E., Freivalds, K., Draguns, A., Gaile, E., Zakovskis, R., Kozlovics, S.: Goal-aware neural SAT solver. In: Proceedings of the 2022 International Joint Conference on Neural Networks (IJCNN 2022) (2022)
Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45–86 (2012)
West, D.: Object Thinking. Microsoft Professional. Microsoft, Redmond (2004)
Zhou, N.-F., Kjellerstrand, H.: The Picat-SAT compiler. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 48–62. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28228-2_4
Acknowledgements
Research supported by the Latvian Council of Science, Project No. 2021/1-0479 “Combinatorial Optimization with Deep Neural Networks”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Kozlovičs, S. (2022). Shared SAT Solvers and SAT Memory in Distributed Business Applications. In: Ivanovic, M., Kirikova, M., Niedrite, L. (eds) Digital Business and Intelligent Systems. Baltic DB&IS 2022. Communications in Computer and Information Science, vol 1598. Springer, Cham. https://doi.org/10.1007/978-3-031-09850-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-031-09850-5_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-09849-9
Online ISBN: 978-3-031-09850-5
eBook Packages: Computer ScienceComputer Science (R0)