Dans cette thèse, nous cherchons à comparer la complexité booléenne classique et la complexité algébrique, en étudiant des problèmes sur les polynômes. Nous considérons les modèles de calcul algébriques de Valiant et de Blum, Shub et Smale (BSS). Pour étudier les classes de complexité algébriques, il est naturel de partir des résultats et des questions ouvertes dans le cas booléen, et de regarder ce qu'il en est dans le contexte algébrique. La comparaison des résultats obtenus dans ces deux domaines permet ainsi d'enrichir notre compréhension des deux théories. La première partie suit cette approche. En considérant un polynôme canoniquement associé à toute formule booléenne, nous obtenons un lien entre les questions de complexité booléenne sur la formule booléenne et les questions de complexité algébrique sur le polynôme. Nous avons étudié la complexité du calcul de ce polynôme dans le modèle de Valiant en fonction de la complexité de la formule booléenne, et avons obtenu des analogues algébriques à certains résultats booléens. Nous avons aussi pu utiliser des méthodes algébriques pour améliorer certains résultats booléens, en particulier de meilleures réductions de comptage. Une autre motivation aux modèles de calcul algébriques est d'offrir un cadre pour l'analyse d'algorithmes continus. La seconde partie suit cette approche. Nous sommes partis d'algorithmes nouveaux pour la recherche de zéros approchés d'un système de n polynômes complexes à n inconnues. Jusqu'à présent il s'agissait d'algorithmes pour le modèle BSS. Nous avons étudié l'implémentabilité de ces algorithmes sur un ordinateur booléen et proposons un algorithme booléen.

by Dimitri P. Bertsekas. / Includes bibliographies. / Research supported by National Science Foundation Grant ENG-79-06332 (87649)

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

Report covers June 1, 1976-July 31, 1978. / Each v. has also a distinctive title. / National Science Foundation. Grant NSF/RANN APR76-12036 National Science Foundation. Grant DAR78-17826

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.