|
This article is cited in 1 scientific paper (total in 1 paper)
Mathematical Foundations of Programming
Front-end algorithm for solving the SAT problem
Yu. M. Smetanin Udmurt State University, Izhevsk, Russia
Abstract:
The algorithm for calculating the semantic value of conjunctive formulas of the form $U = F(X_1, X_2,..., X_n)$ in non-classical propositional logic $L_{S_{2}}$ also calculates the set of all solutions of the logical equation
$$F({x_1}, {x_2},..., {x_n})= 1.$$ Where $F(X_1, X_2,..., X_n)$ — a formula of Boolean algebra of the sets making a discrete Venn diagram. The elements of these sets are non-negative integers.
Based on this algorithm, a new algorithm is built to solve the $ SAT~$ problem. A significant difference between it and a family of algorithms based on $ DPLL $ and
$ CDCL $ is the replacement of Boolean variables with sets. This allows you to effectively check the feasibility of not one, but many sets of values of the logical variables ${x_1}, {x_2},..., {x_n}$.
Key words and phrases:
non-classical propositional logic based on a model with non-degenerate Boolean algebra, calculus of discrete Venn diagrams, problem SAT.
Received: 14.10.2022 Accepted: 10.11.2022
Citation:
Yu. M. Smetanin, “Front-end algorithm for solving the SAT problem”, Program Systems: Theory and Applications, 13:4 (2022), 163–179
Linking options:
https://www.mathnet.ru/eng/ps412 https://www.mathnet.ru/eng/ps/v13/i4/p163
|
Statistics & downloads: |
Abstract page: | 44 | Full-text PDF : | 12 | References: | 12 |
|