Classes de terminale voie générale spécialité NSI.

Ce sujet comporte deux problèmes, totalement indépendants l’un de l’autre.

Lorsque l’écriture de programmes est demandée, ceux-ci devront être rédigés en Python.

Lorsque des requêtes sur des bases de données sont demandées, celles-ci devront être rédigées en SQL.

Durée : 5 heures

1 - Problème : solveur SAT

Ce problème comporte 4 parties qui s’intéressent à l’implémentation d’un solveur SAT (parties 1.2 et 1.3) et à l’expression de contraintes avec des formules (partie 1.4). La partie 1.1 introduit les notations utilisées dans tout le problème. La partie 1.4 est indépendante des deux suivantes. Même si les questions des parties 1.2 et 1.3 sont indépendantes, il est nécessaire d’avoir compris les idées et les notations de la partie 1.2 pour traiter la partie 1.3. Le code peut utiliser des fonctionnalités des questions précédentes même si le candidat ne les a pas traitées.

1.1 - Introduction

1.2 - Un solveur SAT récursif

1.2.1 - Un solveur naïf

1.2.2 - Simplification des clauses unitaires

1.3 - Un solveur itératif

1.3.1 - Retour sur tracé itératif

1.3.2 - « Listes de surveillance » et suppression des appels à la méthode « valeur_formule »

1.3.3 - Simplification des clauses unitaires

1.3.4 - Statistiques sur les formules

1.4 - Un exemple de formule FNC : résolution de sudoku

2 - Problème : mélange de wagons

Dans ce problème, on s’intéresse à des algorithmes qui permettent de réordonner des wagons de trains. Les wagons pouvant uniquement se déplacer le long d’itinéraires prédéfinis, les rails, on souhaite étudier ce qu’il est possible de faire en tenant compte de ces contraintes.

Les wagons d’un train doivent toujours suivre les chemins donnés par les rails. Lorsque deux wagons se suivent sur un même rail, on ne peut en particulier pas changer l’ordre, c’est-à-dire qu’il est impossible pour un wagon de doubler un autre wagon quand les deux sont sur le même rail.

2.1 - Tri avec une voie de stockage

2.2 - Gare de triage

A - Annexes

A.1 - Le solveur naïf

A.2 - Le solveur naïf, avec simplification des clauses unitaires