Geodesic
The length of an unsatisfiable subformula
Algebra i logika, Tome 63 (2024) no. 1, pp. 89-99
Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

We find a bound for the length of a conjunction of some propositional formulas, for which every unsatisfiable formula contains an unsatisfiable subformula. In particular, this technique applies to formulas in conjunctive normal form with restrictions on the number of true literals within every elementary disjunction, as well as for 2-CNFs, for symmetric 3-CNFs, and for conjunctions of voting functions in three literals. A lower bound on the rank of some matrices is used in proofs.
Mots-clés : propositional logic
Keywords: satisfiability, rank of matrix, binary solution. 
@article{AL_2024_63_1_a6,
     author = {A. V. Seliverstov},
     title = {The length of an unsatisfiable subformula},
     journal = {Algebra i logika},
     pages = {89--99},
     year = {2024},
     volume = {63},
     number = {1},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/AL_2024_63_1_a6/}
}
TY  - JOUR
AU  - A. V. Seliverstov
TI  - The length of an unsatisfiable subformula
JO  - Algebra i logika
PY  - 2024
SP  - 89
EP  - 99
VL  - 63
IS  - 1
UR  - http://geodesic.mathdoc.fr/item/AL_2024_63_1_a6/
LA  - ru
ID  - AL_2024_63_1_a6
ER  - 
%0 Journal Article
%A A. V. Seliverstov
%T The length of an unsatisfiable subformula
%J Algebra i logika
%D 2024
%P 89-99
%V 63
%N 1
%U http://geodesic.mathdoc.fr/item/AL_2024_63_1_a6/
%G ru
%F AL_2024_63_1_a6
A. V. Seliverstov. The length of an unsatisfiable subformula. Algebra i logika, Tome 63 (2024) no. 1, pp. 89-99. http://geodesic.mathdoc.fr/item/AL_2024_63_1_a6/

[1] W. Li, C. Xu, Y. Yang, J. Chen, J. Wang, “A refined branching algorithm for the maximum satisfiability problem”, Algorithmica, 84 (2022), 982–1006 | DOI | MR

[2] J. Peng, M. Xiao, “Further improvements for SAT in terms of formula length”, Inform. Comput., 294 (2023), 105085 | DOI | MR

[3] S. Szeider, “Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable”, J. Comput. System Sci., 69:4 (2004), 656–674 | DOI | MR

[4] A. Goerdt, “A threshold for unsatisfiability”, J. Comput. System Sci., 53:3 (1996), 469–486 | DOI | MR

[5] D. Achlioptas, A. Coja-Oghlan, M. Hahn-Klimroth, J. Lee, N. Müller, M. Penschuck, G. Zhou, “The number of satisfying assignments of random 2-SAT formulas”, Random Structures Algorithms, 58:4 (2021), 609–647 | DOI | MR

[6] J. Giráldez-Cruand, J. Levy, “Popularity-similarity random SAT formulas”, Artificial Intelligence, 299 (2021), 103537 | DOI

[7] J. Ding, A. Sly, N. Sun, “Satisfiability threshold for random regular NAE-SAT”, Comm. Math. Phys., 341 (2016), 435–489 | DOI

[8] G. Nie, D. Xu, X. Wang, X. Wang, “The phase transition analysis for the random regular exact 2-(d, k)-SAT problem”, Symmetry, 13:7 (2021), 1231 | DOI

[9] A. A. Boikov, A. V. Seliverstov, “O kube i proektsiyakh podprostranstva”, Vestn. Udmurtskogo un-ta. Matem. Mekh. Kompyut. nauki, 33:3 (2023), 402–415 | DOI

[10] N. T. Kogabaev, “O sistemakh diofantovykh uravnenii nad konechnymi konfiguratsiyami”, Sib. matem. zh., 64:2 (2023), 321–338

[11] M. N. Vyalyi, “Testing the satisfiability of algebraic formulas over the field of two elements”, Probl. Inf. Transm., 59:1 (2023), 57–62 | DOI

[12] A. Abboud, K. Bringmann, D. Hermelin, D. Shabtay, “Scheduling lower bounds via AND subset sum”, J. Comput. System Sci., 127 (2022), 29–40 | DOI