Un espace topologique lié à la SAT: est-il compact?

Le problème de satisfaction est, bien sûr, un problème fondamental en CS théorique. Je jouais avec une version du problème avec une infinité de variables. $\newcommand{\sat}{\mathrm{sat}} \newcommand{\unsat}{\mathrm{unsat}}$

Configuration de base. Soit $X$ un ensemble de variables non vide et éventuellement infini . Un littéral est soit une variable $x \in X$ soit sa négation $\neg x$ . Une clause $c$ est une disjonction d' un nombre fini de littéraux . Enfin, nous définissons une formule $F$ comme un ensemble de clauses .

Une affectation de $X$ est une fonction $\sigma : X \to \{0,1\}$ . Je ne définirai pas explicitement la condition à laquelle une affectation $\sigma$ satisfait une clause; il est légèrement encombrant et identique à celui du SAT standard. Enfin, une affectation satisfait une formule si elle satisfait toutes les clauses constitutives. Soit $\sat(F)$ l'ensemble des affectations satisfaisantes pour $F$ , et soit $\unsat(F)$ le complément de $\sat(F)$ .

Un espace topologique.

Notre objectif est de doter l'espace de toutes les affectations de $X$ , appelons ceci $\Sigma$ , d'une structure topologique . Nos ensembles fermés sont de la forme $\sat(F)$ où $F$ est une formule. On peut vérifier qu'il s'agit bien d'une topologie:

• La formule vide $\emptyset$ ne contenant aucune clause est satisfaite par toutes les affectations; donc $\Sigma$ est fermé.
• La formule $\{ x, \neg x \}$ pour tout $x \in X$ est une contradiction. Donc $\emptyset$ est fermé.
• Fermeture sous intersection arbitraire. Supposons $F_{i}$ est une formule pour chaque $i \in I$ . Alors $\sat \left(\bigcup_{i \in I} F_i\right) = \bigcap_{i \in I} \sat(F_i)$ .
• Fermeture sous union finie. Supposons que $F$ et $G$ sont deux formules et définissent $$F \vee G := \{ c \vee d \,:\, c \in F, d \in G \}.$$ Alors $\sat(F \vee G) = \sat(F) \cup \sat(G)$ . Cela nécessite un argument, mais je vais sauter ceci.

Appelez cette topologie $\mathcal T$ , la "topologie de satisfiabilité" (!) Sur $\Sigma$ . Bien sûr, les ensembles ouverts de cette topologie sont de la forme \ unsat (F)$\unsat(F)$ . De plus, je remarquai que la collection d'ensembles ouverts

Compact? Je pense que c'est une façon intéressante, sinon terriblement utile, de voir les choses. Je veux comprendre si cet espace topologique possède des propriétés traditionnelles intéressantes comme la compacité, la connectivité, etc. Dans cet article, nous nous limiterons à la compacité:

Soit une collection infiniment dénombrable de variables. ¹ Est compact sous ?Σ $X$$\Sigma$$\mathcal T$

On peut prouver ce qui suit

Proposition. est compact si et seulement pour toutes les formules insatisfiables , il existe une sous - formule insatisfiables finie .$\mathcal T$$F$$\{ c_1, c_2, \ldots, c_m \} \subseteq F$

(Exercice pas si difficile!) Après plusieurs jours de réflexion, je n'ai pas beaucoup progressé pour répondre à cette question. Je n'ai pas non plus de preuves solides pour ou contre la compacité. Pouvez-vous suggérer une approche?

Enfin, comme question bonus:

Une telle structure a-t-elle été étudiée auparavant?

¹ La restriction à dénombrable est juste pour la simplicité; cela ressemble aussi à la prochaine étape naturelle à partir d'un nombre fini de variables.$X$

Ce que vous faites est de dériver une représentation topologique d'une algèbre booléenne. L'étude des représentations des algèbres booléennes remonte au moins à Lindenbaum et Tarski qui ont prouvé (en 1925, je pense) que les algèbres booléennes atomiques complètes sont isomorphes aux réseaux de jeux de puissance.

Il existe cependant des algèbres booléennes qui ne sont pas complètes et atomiques. Par exemple, la séquence , est une chaîne descendante qui n'a pas de limite dans l'algèbre booléenne définie sur des formules. La question de savoir si des algèbres booléennes arbitraires, comme celle que vous mentionnez, avait également des représentations basées sur des ensembles a été résolue par Marshall Stone , qui a avancé la maxime "toujours topologiser" (Marshall H. Stone. La représentation des algèbres booléennes , 1938) .$x_1, x_1 \land x_2, \ldots$

Théorème de représentation de Stone pour les algèbres booléennes Chaque algèbre booléenne est isomorphe au réseau de sous-ensembles clopen d'un espace topologique.

L'idée principale est de considérer quelles sont dans votre cas les affectations satisfaisantes d'une formule. Dans le cas général, vous considérez les homomorphismes d'une algèbre booléenne dans l'algèbre booléenne à deux éléments (les valeurs de vérité). L'inverse de vous donne les ensembles de missions satisfaisant, ou ce qu'on appelle ultrafiltres de l'algèbre booléenne. À partir de ceux-ci, on peut obtenir une topologie appelée spectre ou espace de pierre d'une algèbre booléenne. Stone répond également à votre question.$\mathit{true}$

L'espace de pierre d'une algèbre booléenne est un espace de Hausdorff compact et totalement déconnecté.

Plusieurs résultats ont étendu et généralisé la représentation de Stone dans différentes directions. Une question naturelle est de se demander si d'autres familles de réseaux ont de telles représentations. Les résultats de Stone s'appliquent également aux réseaux distributifs. Alasdair Urquhart a donné des représentations topologiques pour les réseaux arbitraires en 1978. Les réseaux distributifs jouissent d'une plus grande diversité de structure par rapport aux algèbres de Boole et présentent un grand intérêt. Hilary Priestley a donné une représentation différente du cas distributif en 1970, en utilisant l'idée d'un espace topologique ordonné . Au lieu de représentations basées sur des ensembles, nous pouvons trouver des représentations et des topologies basées sur des posets.

Les constructions de ces papiers ont une propriété remarquable. La construction de Stone ne mappe pas seulement les algèbres booléennes aux espaces topologiques: les relations structurelles reliant les algèbres booléennes se traduisent en propriétés structurelles entre les topologies résultantes. C'est une dualité entre les catégories. Toute la gamme de ces résultats s'appelle Stone Duality . Informellement, les dualités nous donnent des traductions précises entre les univers mathématiques: le monde combinatoire des ensembles, le monde algébrique des réseaux, le monde spatial de la topologie et le monde déductif de la logique. Voici quelques points de départ qui peuvent vous aider.

1. Le chapitre 11 de Introduction to Lattices and Order , par Davey et Priestley, couvre le théorème de Stone.
2. Les diapositives de Matthew Gwynne couvrent le théorème et donnent une preuve de compacité. Matthew (dans les commentaires) suggère également l' introduction aux algèbres booléennes par Paul Halmos.
3. En passant de la logique propositionnelle à la logique modale, l'algèbre booléenne est étendue avec un opérateur préservant les jointures et une topologie avec un intérieur. L'article de Jónsson et Tarski, 1952, Algèbres booléennes avec opérateurs est extrêmement lisible et conforme à la notation moderne.
4. Le chapitre 5 de Modal Logic de Blackburn, de Rijke et Venema couvre le théorème de Stone et son extension aux algèbres booléennes avec des opérateurs.
5. Stone Spaces de Peter Johnstone examine ces résultats pour divers autres types d'algèbres.