The Satisfiability problem is, of course, a fundamental problem in theoretical CS. I was playing with one version of the problem with infinitely many variables. $\newcommand{\sat}{\mathrm{sat}} \newcommand{\unsat}{\mathrm{unsat}}$
Basic Setup. Let $X$ be a nonempty and possibly infinite set of variables. A literal is either a variable $x \in X$ or its negation $\neg x$. A clause $c$ is a disjunction of finite number of literals. Finally, we define a formula $F$ as a set of clauses.
An assignment of $X$ is a function $\sigma : X \to \{0,1\}$. I will not explicitly define the condition for when an assignment $\sigma$ satisfies a clause; it is slightly cumbersome, and is the same as in standard SAT. Finally, an assignment satisfies a formula if it satisfies every constituent clause. Let $\sat(F)$ be the set of satisfying assignments for $F$, and let $\unsat(F)$ be the complement of $\sat(F)$.
A topological space.
Our goal is to endow the space of all assignments of $X$, call this $\Sigma$, with a topological structure. Our closed sets are of the form $\sat(F)$ where $F$ is a formula. We can verify that this is indeed a topology:
- The empty formula $\emptyset$ containing no clauses is satisfied by all assignments; so $\Sigma$ is closed.
- The formula $\{ x, \neg x \}$ for any $x \in X$ is a contradiction. So $\emptyset$ is closed.
- Closure under arbitrary intersection. Suppose $F_{i}$ is a formula for each $i \in I$. Then $\sat \left(\bigcup_{i \in I} F_i\right) = \bigcap_{i \in I} \sat(F_i)$.
- Closure under finite union. Suppose $F$ and $G$ are two formulas, and define $$ F \vee G := \{ c \vee d \,:\, c \in F, d \in G \}. $$ Then $\sat(F \vee G) = \sat(F) \cup \sat(G)$.This needs an argument, but I'll skip this.
Call this topology $\mathcal T$, the "satisfiability topology"(!) on $\Sigma$. Of course, the opens sets of this topology are of the form $\unsat(F)$. Moreover, I observed that the collection of open sets $$ \{ \unsat(c) \,:\, c \text{ is a clause} \} $$ forms a basis for $\mathcal T$. (Exercise!)
Compact? I feel that this is an interesting, if not terribly useful, way to look at things. I want to understand whether this topological space possesses traditional interesting properties like compactness, connectedness etc. In this post, we will restrict ourselves to compactness:
Let $X$ be a countably infinite collection of variables.1 Is $\Sigma$ compact under $\mathcal T$?
One can prove the following
Proposition. $\mathcal T$ is compact if and only for all unsatisfiable formulas $F$, there exists a finite unsatisfiable subformula $\{ c_1, c_2, \ldots, c_m \} \subseteq F$.
(Not-so-hard exercise!) After several days of thinking, I do not have much progress in answering this question. I also do not have strong evidence for or against compactness. Can you suggest some approach?
Finally, as a bonus question:
Has such a structure been studied before?
1The restriction to countable $X$ is just for simplicity; it also feels like the next natural step from finite number of variables.