Polyominos, pavages et solveurs SAT - Historique des versions

Malabre : les balise sont pas les bonnes

2025-05-11T21:59:29Z

les balise sont pas les bonnes

← Version précédente		Version du 11 mai 2025 à 21:59
Ligne 23 :		Ligne 23 :
	</pre>		</pre>

	~~Ceci~~ correspond à :		Cela correspond à :

	<pre>		<pre>
Ligne 44 :		Ligne 44 :
	=== Lecture de la grille ===		=== Lecture de la grille ===

			<pre>
	<syntaxhighlight lang="python">
	def lecteur_tab(file: str) -> list:		def lecteur_tab(file: str) -> list:
	...		...
			</pre>
	</syntaxhighlight>

	Retourne la liste des coordonnées des cases utilisables dans la grille (les <code>#</code>).		Retourne la liste des coordonnées des cases utilisables dans la grille (les <code>#</code>).
Ligne 59 :		Ligne 59 :
	=== Vérification de placements valides ===		=== Vérification de placements valides ===

			<pre>
	<syntaxhighlight lang="python">
	def verif_version(origine, pieces, tab) -> list:		def verif_version(origine, pieces, tab) -> list:
	...		...
			</pre>
	</syntaxhighlight>

	Retourne les versions valides de la pièce à une position donnée (~~celles~~ qui restent dans la grille).		Retourne les versions valides de la pièce à une position donnée (qui restent dans la grille).

	== Génération de clauses ==		== Génération de clauses ==
Ligne 70 :		Ligne 70 :
	=== Clause de placement ===		=== Clause de placement ===

			<pre>
	<syntaxhighlight lang="python">
	def creation_clause_tab(piece, tab) -> str:		def creation_clause_tab(piece, tab) -> str:
	...		...
			</pre>
	</syntaxhighlight>

	Exemple de clause :		Exemple de clause :
Ligne 87 :		Ligne 87 :
	Empêche que deux pièces différentes recouvrent la même case.		Empêche que deux pièces différentes recouvrent la même case.

			<pre>
	<syntaxhighlight lang="python">
	def creation_contrainte_unicite(tab, piece) -> str:		def creation_contrainte_unicite(tab, piece) -> str:
	...		...
			</pre>
	</syntaxhighlight>

	Exemple :		Exemple :
Ligne 102 :		Ligne 102 :
	Impose qu’au moins une pièce couvre chaque case.		Impose qu’au moins une pièce couvre chaque case.

			<pre>
	<syntaxhighlight lang="python">
	def creation_contrainte_couverture(tab, piece) -> str:		def creation_contrainte_couverture(tab, piece) -> str:
	...		...
			</pre>
	</syntaxhighlight>

	Exemple :		Exemple :
Ligne 115 :		Ligne 115 :
	=== Clause de couverture complète ===		=== Clause de couverture complète ===

			<pre>
	<syntaxhighlight lang="python">
	def creation_clause_complet(tab) -> str:		def creation_clause_complet(tab) -> str:
	...		...
			</pre>
	</syntaxhighlight>

	Assure que chaque case utile est bien prise en compte.		Assure que chaque case utile est bien prise en compte.
Ligne 134 :		Ligne 134 :
	Soit la pièce suivante :		Soit la pièce suivante :

			<pre>
	<syntaxhighlight lang="python">
	piece = [[0,0], [0,1], [0,2], [1,2]]		piece = [[0,0], [0,1], [0,2], [1,2]]
			</pre>
	</syntaxhighlight>

	Et une grille donnée dans le fichier <code>tab.txt</code>. En exécutant :		Et une grille donnée dans le fichier <code>tab.txt</code>. En exécutant :

			<pre>
	<syntaxhighlight lang="python">
	tab = lecteur_tab("tab.txt")		tab = lecteur_tab("tab.txt")
	generates_clauses(piece, tab)		generates_clauses(piece, tab)
			</pre>
	</syntaxhighlight>

	On obtient le fichier <code>clausepavage.txt</code> contenant les contraintes.		On obtient le fichier <code>clausepavage.txt</code> contenant les contraintes.

Malabre le 11 mai 2025 à 21:58

2025-05-11T21:58:14Z

Voir les modifications

Malabre le 11 mai 2025 à 21:56

2025-05-11T21:56:23Z

← Version précédente		Version du 11 mai 2025 à 21:56
Ligne 133 :		Ligne 133 :


	code complet disponible sur le ~~(github)~~[https://github.com/lasnelus/visi201]		code complet disponible sur le [https://github.com/lasnelus/visi201 github]

Malabre : /* Clause de couverture complète */

2025-05-11T21:55:46Z

Clause de couverture complète

← Version précédente		Version du 11 mai 2025 à 21:55
Ligne 133 :		Ligne 133 :


	code complet disponible sur le ~~[github]~~(https://github.com/lasnelus/visi201)		code complet disponible sur le (github)[https://github.com/lasnelus/visi201]

Malabre le 11 mai 2025 à 21:55

2025-05-11T21:55:25Z

← Version précédente		Version du 11 mai 2025 à 21:55
Ligne 130 :		Ligne 130 :

	On obtiendras le fichier <code>clausepavage.txt</code> avec les contraintes.		On obtiendras le fichier <code>clausepavage.txt</code> avec les contraintes.



			code complet disponible sur le [github](https://github.com/lasnelus/visi201)

Malabre le 11 mai 2025 à 21:54

2025-05-11T21:54:01Z

← Version précédente		Version du 11 mai 2025 à 21:54
Ligne 41 :		Ligne 41 :

	=== Lecture de la grille ===		=== Lecture de la grille ===
			<code>
	<syntaxhighlight lang="python">
	def lecteur_tab(file: str) -> list:		def lecteur_tab(file: str) -> list:
	...		...
			</code>
	</syntaxhighlight>

	Retourne la liste des coordonnées des cases utilisables dans la grille (les <code>#</code>).		Retourne la liste des coordonnées des cases utilisables dans la grille (les <code>#</code>).
Ligne 55 :		Ligne 55 :

	=== Vérification de placements valides ===		=== Vérification de placements valides ===
			<code>
	<syntaxhighlight lang="python">
	def verif_version(origine, pieces, tab) -> list:		def verif_version(origine, pieces, tab) -> list:
	...		...
			</code>
	</syntaxhighlight>

	Retourne les versions valides de la pièce à une position donnée (qui restent dans la grille).		Retourne les versions valides de la pièce à une position donnée (qui restent dans la grille).
Ligne 65 :		Ligne 65 :

	=== Clause de placement ===		=== Clause de placement ===
			<code>
	<syntaxhighlight lang="python">
	def creation_clause_tab(piece, tab) -> str:		def creation_clause_tab(piece, tab) -> str:
	...		...
			</code>
	</syntaxhighlight>

	Exemple de clause :		Exemple de clause :
Ligne 79 :		Ligne 79 :
	Empêche que deux pièces différentes recouvrent la même case.		Empêche que deux pièces différentes recouvrent la même case.

			<code>
	<syntaxhighlight lang="python">
	def creation_contrainte_unicite(tab, piece) -> str:		def creation_contrainte_unicite(tab, piece) -> str:
	...		...
			</code>
	</syntaxhighlight>

	Exemple :		Exemple :
Ligne 92 :		Ligne 92 :
	Impose qu’au moins une pièce couvre chaque case.		Impose qu’au moins une pièce couvre chaque case.

			<scode>
	<syntaxhighlight lang="python">
	def creation_contrainte_couverture(tab, piece) -> str:		def creation_contrainte_couverture(tab, piece) -> str:
	...		...
			</code>
	</syntaxhighlight>

	Exemple :		Exemple :
Ligne 103 :		Ligne 103 :

	=== Clause de couverture complète ===		=== Clause de couverture complète ===
			<code>
	<syntaxhighlight lang="python">
	def creation_clause_complet(tab) -> str:		def creation_clause_complet(tab) -> str:
	...		...
			</code>
	</syntaxhighlight>

	Assure que chaque case utile est bien prise en compte.		Assure que chaque case utile est bien prise en compte.
Ligne 119 :		Ligne 119 :

	Soit la pièce suivante :		Soit la pièce suivante :
			<code>
	<syntaxhighlight lang="python">
	piece = [[0,0], [0,1], [0,2], [1,2]]		piece = [[0,0], [0,1], [0,2], [1,2]]
			</code>
	</syntaxhighlight>

	Et une grille donnée dans <code>tab.txt</code>. En exécutant :		Et une grille donnée dans <code>tab.txt</code>. En exécutant :
			<code>
	<syntaxhighlight lang="python">
	tab = lecteur_tab("tab.txt")		tab = lecteur_tab("tab.txt")
	generates_clauses(piece, tab)		generates_clauses(piece, tab)
			</code>
	</syntaxhighlight>

	Tu obtiendras le fichier <code>clausepavage.txt</code> avec les contraintes.		On obtiendras le fichier <code>clausepavage.txt</code> avec les contraintes.

Malabre le 11 mai 2025 à 21:52

2025-05-11T21:52:17Z

← Version précédente		Version du 11 mai 2025 à 21:52
Ligne 116 :		Ligne 116 :
	C_2_0		C_2_0
	</pre>		</pre>


			Soit la pièce suivante :
			<syntaxhighlight lang="python">
			piece = [[0,0], [0,1], [0,2], [1,2]]
			</syntaxhighlight>

			Et une grille donnée dans <code>tab.txt</code>. En exécutant :
			<syntaxhighlight lang="python">
			tab = lecteur_tab("tab.txt")
			generates_clauses(piece, tab)
			</syntaxhighlight>

			Tu obtiendras le fichier <code>clausepavage.txt</code> avec les contraintes.

Malabre le 11 mai 2025 à 21:51

2025-05-11T21:51:27Z

← Version précédente		Version du 11 mai 2025 à 21:51
Ligne 38 :		Ligne 38 :
	* la contrainte qu'elle ne soit couverte '''qu'une seule fois''',		* la contrainte qu'elle ne soit couverte '''qu'une seule fois''',
	* l’implication logique entre une pièce placée et les cases couvertes.		* l’implication logique entre une pièce placée et les cases couvertes.


			=== Lecture de la grille ===
			<syntaxhighlight lang="python">
			def lecteur_tab(file: str) -> list:
			...
			</syntaxhighlight>

			Retourne la liste des coordonnées des cases utilisables dans la grille (les <code>#</code>).


			=== Manipulation des pièces ===
			* <code>trouve_origine(piece)</code> : Trouve le coin supérieur gauche de la pièce.
			* <code>placement_piece(origine, piece)</code> : Calcule la pièce translatée selon une origine.
			* <code>version_piece(piece)</code> : Retourne les 8 versions (rotations et symétries) d’une pièce.

			=== Vérification de placements valides ===
			<syntaxhighlight lang="python">
			def verif_version(origine, pieces, tab) -> list:
			...
			</syntaxhighlight>

			Retourne les versions valides de la pièce à une position donnée (qui restent dans la grille).

			== Génération de clauses ==

			=== Clause de placement ===
			<syntaxhighlight lang="python">
			def creation_clause_tab(piece, tab) -> str:
			...
			</syntaxhighlight>

			Exemple de clause :
			<pre>
			~P0_2_1 C_3_1
			</pre>
			(signifie : si la version 0 de la pièce est placée à (2,1), alors la case (3,1) est couverte)

			=== Contrainte d’unicité ===
			Empêche que deux pièces différentes recouvrent la même case.

			<syntaxhighlight lang="python">
			def creation_contrainte_unicite(tab, piece) -> str:
			...
			</syntaxhighlight>

			Exemple :
			<pre>
			~P1_0_1 ~P2_1_1
			</pre>

			=== Contrainte de couverture ===
			Impose qu’au moins une pièce couvre chaque case.

			<syntaxhighlight lang="python">
			def creation_contrainte_couverture(tab, piece) -> str:
			...
			</syntaxhighlight>

			Exemple :
			<pre>
			P0_0_0 P1_1_0
			</pre>

			=== Clause de couverture complète ===
			<syntaxhighlight lang="python">
			def creation_clause_complet(tab) -> str:
			...
			</syntaxhighlight>

			Assure que chaque case utile est bien prise en compte.

			Exemple :
			<pre>
			C_0_0
			C_1_0
			C_2_0
			</pre>

Malabre le 11 mai 2025 à 21:49

2025-05-11T21:49:23Z

← Version précédente		Version du 11 mai 2025 à 21:49
Ligne 25 :		Ligne 25 :
	(A ∨ B ∨ ¬C) ∧ (¬A ∨ D)		(A ∨ B ∨ ¬C) ∧ (¬A ∨ D)
	</pre>		</pre>

			== Représentation du problème ==

			Pour représenter un problème de pavage :

			# Une '''forme''' (ou grille) est décrite dans un fichier <code>tab.txt</code>, où les cases utilisables sont indiquées par le caractère <code>#</code>.
			# Une '''pièce''' est décrite par une liste de coordonnées relatives comme <code>[[0,0], [0,1], [0,2], [1,2]]</code>.

			Nous générons alors toutes les clauses logiques qui modélisent :
			* les positions valides des pièces,
			* la contrainte que chaque case soit couverte au '''moins une fois''',
			* la contrainte qu'elle ne soit couverte '''qu'une seule fois''',
			* l’implication logique entre une pièce placée et les cases couvertes.

Malabre le 11 mai 2025 à 21:48

2025-05-11T21:48:29Z

← Version précédente		Version du 11 mai 2025 à 21:48
Ligne 11 :		Ligne 11 :

	== Utilisation de SAT13 ==		== Utilisation de SAT13 ==
	`SAT13` est un solveur qui accepte une formule logique en forme normale conjonctive (FNC), composée uniquement d'opérations ET, OU et NON. Plus précisément :		<code>SAT13</code> est un solveur qui accepte une '''formule logique en forme normale conjonctive (FNC)''', composée uniquement d'opérations '''ET''', '''OU''' et '''NON'''. Plus précisément :

	- Chaque ligne représente une clause (un OU logique entre plusieurs littéraux).		* Chaque '''ligne''' représente une clause (un '''OU''' logique entre plusieurs littéraux).
		⚫	* L’ensemble des lignes est évalué comme un '''ET''' logique.
		⚫	* Un littéral est soit une variable, soit sa négation (utilisant le symbole <code>~</code>).

			<pre>
⚫	- L’ensemble des lignes est évalué comme un ET logique.
			A B ~C

			~A D
⚫	- Un littéral est soit une variable, soit sa négation (utilisant le symbole `~`).
			</pre>
			Ceci correspond à :
			<pre>
			(A ∨ B ∨ ¬C) ∧ (¬A ∨ D)
			</pre>