Geodesic
The length of an unsatisfiable subformula
Algebra i logika, Tome 63 (2024) no. 1, pp. 89-99

Voir la notice de l'article provenant de la source Math-Net.Ru

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},
     publisher = {mathdoc},
     volume = {63},
     number = {1},
     year = {2024},
     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
PB  - mathdoc
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
%I mathdoc
%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/