Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Problème SAT

Séances de cours associées (31)

Logique de prédicat: Résumé de la semaine 2

Couvre le concept de l'univers du discours et des valeurs de vérité dans la logique prédictive.

Preuves formelles: vérification des invariants et des modèles liés

Explore les preuves formelles, les problèmes de satisfaisabilité et les invariants inductifs en utilisant des requêtes SAT dans des circuits séquentiels.

Élimination de l'arithmétique et des quantificateurs de Presbourg

Couvre l'arithmétique de Presbourg, l'élimination des quantificateurs et la transformation des formules en forme normale disjonctive.

Automatiser les preuves logiques de premier ordre en utilisant la résolution

Couvre la syntaxe logique de premier ordre, la sémantique et la résolution pour les propriétés de preuve.

Complexité des algorithmes : notation Big-O

Explore la complexité de l'algorithme, la notation big-O, l'induction, la récursion et l'analyse des temps de fonctionnement, couvrant les problèmes NP et les classes de complexité.

Théorie de calcul: Décidabilité et complexité Connectez-vous à Mediaspace pour regarder cette vidéo

S'inscrit dans la théorie du calcul, couvrant la décidabilité, la complexité, P vs. NP, et les réductions.

Problème de satisfabilité booléenne : résoudre les techniques Connectez-vous à Mediaspace pour regarder cette vidéo

Explore le problème de satisfabilité booléenne et l'algorithme Davis-Putnam-Logemann-Loveland, ainsi que les résolveurs SAT modernes et les techniques de résolution efficaces.

La satisfaction et les clusters Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre le seuil de satisfaisabilité, les clusters de solutions, le paramètre alpha et le calcul de cluster moyen.

Logique principale : quantificateurs et formulaires normaux Connectez-vous à Mediaspace pour regarder cette vidéo

Explore la logique prédictive, en mettant l'accent sur les quantificateurs et les formes normales, soulignant l'importance de trouver des témoins et des contre-exemples.

Modèles de marché financier : arbitrage et exhaustivité Connectez-vous à Mediaspace pour regarder cette vidéo

Explore des modèles de marché financier sans arbitrage et complets, des probabilités neutres sur le plan du risque, des prix structurés des billets et des options de couverture.

Modèles stochastiques pour les communications: Chaînes Markov à temps discret - Temps d'absorption Connectez-vous à Mediaspace pour regarder cette vidéo

Discute des chaînes Markov à temps discret et du temps d'absorption dans les systèmes de communication.