Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

Graph
Search

fr|en

Se Connecter

Concept

Problème SAT

Résumé

vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité. Il a été mis en lumière par le théorème de Cook, qui est à la base de la théorie de la NP-complétude et du problème P = NP. Le problème SAT a aussi de nombreuses applications notamment en satisfaction de contraintes, planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation : on se ramène à des formules propositionnelles et on utilise un . Terminologie Formules de la logique propositionnelle Logiqu

Source officielle

https://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (57)

Publications associées

Chargement

Personnes associées (11)

Personnes associées

Chargement

Unités associées (5)

Unités associées

Chargement

Concepts associés (59)

vignette|Quelques classes de complexité étudiées dans le domaine de la théorie de la complexité. Par exemple, P est la classe des problèmes décidés en temps polynomial par une machine de Turing déterm

vignette|400px|Représentation visuelle des deux configurations possibles. Le problème P ≟ NP est une conjecture en mathématiques, et plus précisément en informatique théorique, considérée par de nomb

En théorie de la complexité, un problème NP-complet ou problème NPC (c'est-à-dire un problème complet pour la classe NP) est un problème de décision vérifiant les propriétés suivantes :

il est pos

Afficher plus

Concepts associés

Chargement

Cours associés (14)

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

The study of random walks finds many applications in computer science and communications. The goal of the course is to get familiar with the theory of random walks, and to get an overview of some applications of this theory to problems of interest in communications, computer and network science.

Ce cours présente une introduction aux méthodes d'approximation utilisées pour la simulation numérique en mécanique des fluides. Les concepts fondamentaux sont présentés dans le cadre de la méthode des différences finies puis étendus à celles des éléments finis et spectraux.

Afficher plus

Cours associés

Chargement

Séances de cours associées (27)

Séances de cours associées

Chargement

Asynchronous updates for stochastic gradient descent

Alberto Silvio Chiappa

Finding convergence rates for numerical optimization algorithms is an important task, because it gives a justification to their use in solving practical problems, while also providing a way to compare their efficiency. This is especially useful in an asynchronous environment, because the algorithms are often proven to be more efficient than their synchronous counterparts by experience, but they lack the theory that justifies this property. Furthermore, analyzing the various issues that can arise when inconsistency is taken into consideration, it is possible to obtain a clearer picture of the downsides of inexact implementations one should be aware of. This work tries to address the problem of finding an expected convergence rate for the asynchronous version of the widely popular stochastic gradient descent algorithm, applied to the common class of problems that present a cost function with a sum structure. It follows a similar approach to the one suggested by R. Leblond, F. Pedregosa and S. Lacoste-Julien in "ASAGA: Asynchronous Parallel SAGA" (2016) [RLLJ16], also borrowing their formalization of asynchronicity. The main achievement of this work is a bound on the constant step size that guarantees convergence in expectation of the algorithm. The relative convergence rate is also obtained. The result is also partially validated by sequential models of an asynchronous environment. We hope that this can be a basis for future applications of the same approach to more specific algorithms and that numerical experiments on real multiprocessor architecture can be performed in the future to further validate the convergence rates.

2017

Chargement

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragment is independentof the base element and index set theories.

Springer, Cham2022

Chargement

Simulation numérique des phénomènes thermiques et magnétohydrodynamiques dans une cellule de Hall-Héroult

Yasser Safa

This work is concerned with a numerical simulation of the thermal behaviour of an electrolysis cell for the production of the aluminium. Aluminium is produced by an electrolytic reduction of alumina dissolved in a bath of molten cryolite. In this reduction process, called Hall-Héroult process, the metal is produced at about 965 °C. A frozen bath layer, called ledge, arises in the boundary region and protects the side walls of the cell from corrosive electrolyte. This ledge may change the magnetohydrodynamical equilibrium of the cell and reduce the heat loss through the walls. The ledge is thus playing a significant role in both the thermal and magnetohydrodynamical behaviour of the cell. A precise knowledge of the ledge is thus an imporant ingredient in the optimization process of the cell. The temperature field and the ledge shape in a whole smelter are obtained by simultaneously solving the system of equations formed by: a non-linear convection-diffusion heat equation, which can be considered as a Stephan problem in enthalpy and temperature in the domain of the cell occupied by fluids and ledge, Navier-Stokes equations with a free interface in the fluid domains and Maxwell equations in the whole space. The source term of the heat equation results from the Joule effect due to the electrical current crossing the cell. A Chernoff scheme is used to numerically solve Stephan problem. Three dimensional numerical calculations showing ledge shape, temperature and velocity fields as well as electrical potential for an operating cell are obtained. The effect of thermal field on the electrical current and the effect of fluid motions on the ledge shape in the aluminium cells are presented.

EPFL2005

Chargement