Sur les problèmes de complexité en déduction automatique : base de Hilbert, modèles uniques et minimaux

Abstract : In this thesis we are interested in the complexity of sorne problems in the framework of automated deduction. We study the computational complexity of counting the Hilbert basis of a homogeneous system of linear diophantine equations. The Hilbert basis of a homogeneous system of linear Diophantine equations over non-negative integers is the set of aIl non-zero vectors that are minimal solutions. We establish lower and upper bounds for the complexity of this problem, by showing that counting the Hilbert basis is #P-hard and belongs to the class #NP. Moreover, we investigate the complexity of variants obtained by restricting the number of occurrences of the variables in the system. We also study the problem of recognizing the Hilbert basis. We analyze the problem of the Hilbert basis where the coefficients are given in unary notation. We prove that deciding whether a given solution belongs to the Hilbert basis of a given system is a coNP-complete problem in the strong sense. Furthermore, we show that given a linear Diophantine system and a set of solutions, as king whether this set represents the Hilbert basis of the system is polynomialy equivalent to the problem of deciding whether a glven set of vectors constitutes the Hilbert basis of an unknown linear Diophantine system. We also study the unique satisfiability problem that consists of deciding if there exists a unique solution to a given propositional formula. We give a dichotomy theorem for this problem by partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_1999_0254_JUBAN.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01747275
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:56:23 AM
Last modification on : Tuesday, April 24, 2018 - 1:30:19 PM

Identifiers

  • HAL Id : tel-01747275, version 1

Collections

Citation

Laurent Juban. Sur les problèmes de complexité en déduction automatique : base de Hilbert, modèles uniques et minimaux. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1999. Français. ⟨NNT : 1999NAN10254⟩. ⟨tel-01747275⟩

Share

Metrics

Record views

24