[proofplan] We first check in polynomial time that the input is a well-formed Boolean formula in conjunctive normal form and that every clause is a Horn clause; malformed inputs and non-Horn inputs are rejected. For a valid Horn formula, we convert each Horn clause into an implication whose premise is a conjunction of variables and whose conclusion is either a variable or the contradiction symbol $\bot$. Starting from the all-false assignment, we repeatedly force variables to be true whenever an implication has all premises true, and reject if an implication forcing $\bot$ has all premises true. The process terminates in polynomial time because each variable is changed from false to true at most once, and the final closure assignment satisfies the formula exactly when no contradiction rule fires. [/proofplan] [step:Reject malformed inputs and non-Horn formulas] Let $w$ be the finite input string under the chosen standard encoding of Boolean formulas. A deterministic parser first checks whether $w$ encodes a well-formed Boolean formula in conjunctive normal form. If it does not, the algorithm rejects. If it does, the parser lists the clauses and, for each clause, counts the number of positive literals. If some clause has more than one positive literal, the algorithm rejects. This check scans the input and its parsed clause list using time bounded by a polynomial in the input length. Therefore the remaining steps may assume that the input is a Horn formula in conjunctive normal form, and rejecting earlier inputs is correct because such inputs are not encodings of satisfiable Horn formulas. [/step] [step:Rewrite each Horn clause as an implication rule] Let $\varphi$ be a Horn formula, meaning a conjunctive normal form formula whose clauses each contain at most one positive literal. Let $V := \{x_1,\dots,x_n\}$ denote the finite set of variables appearing in $\varphi$. We write $\bot$ for the always-false contradiction symbol and $\top$ for the always-true formula. Each clause of $\varphi$ with a positive literal has the form $\neg x_{i_1} \vee \cdots \vee \neg x_{i_k} \vee y$, where $k \geq 0$, the variables $x_{i_1},\dots,x_{i_k},y$ lie in $V$, and $y$ is the unique positive literal in the clause. This clause is logically equivalent to the implication rule $x_{i_1} \land \cdots \land x_{i_k} \to y$. A Horn clause with no positive literal has the form $\neg x_{i_1} \vee \cdots \vee \neg x_{i_k}$ and is logically equivalent to the contradiction rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$. When $k=0$, the empty conjunction is interpreted as true. Thus a positive unit clause $y$ becomes $\top \to y$, and the empty clause becomes $\top \to \bot$. Let $R_+$ denote the finite set of implication rules with conclusions in $V$, and let $R_\bot$ denote the finite set of implication rules with conclusion $\bot$. [/step] [step:Run the forward-chaining algorithm from the all-false assignment] Define a truth assignment $a: V \to \{0,1\}$ initially by $a(x)=0$ for every $x \in V$. Repeatedly perform the following operation: if there is a rule $x_{i_1} \land \cdots \land x_{i_k} \to y$ in $R_+$ such that $a(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$ and $a(y)=0$, then redefine $a(y):=1$. If at any point there is a rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$ in $R_\bot$ such that $a(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$, reject. If no further positive rule can force a new variable to become true and no contradiction rule has fired, accept. [guided] The algorithm is a closure procedure. We begin with the smallest possible assignment, namely the assignment $a: V \to \{0,1\}$ defined by $a(x)=0$ for every variable $x \in V$. A positive rule $x_{i_1} \land \cdots \land x_{i_k} \to y$ says that once all variables $x_{i_1},\dots,x_{i_k}$ have become true, the variable $y$ is forced to be true in every satisfying assignment. Therefore, whenever $a(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$ and still $a(y)=0$, we update the assignment by setting $a(y):=1$. A contradiction rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$ means that no satisfying assignment may make all variables $x_{i_1},\dots,x_{i_k}$ true simultaneously. Thus if the current assignment has $a(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$, the formula cannot be satisfied by any assignment extending the forced truths already derived, and the algorithm rejects. The convention about the empty conjunction is important. If $k=0$, then the premise is true without requiring any variable. Thus a rule $\top \to y$ forces $y$ immediately, while a rule $\top \to \bot$ is an immediate contradiction. [/guided] [/step] [step:Show the forward-chaining process runs in polynomial time] Let $N$ be the length of the input formula $\varphi$, measured as the total number of literal occurrences plus the number of clauses. Each variable changes value from $0$ to $1$ at most once, so at most $n \leq N$ successful variable updates occur. The rules can be stored with a counter for each premise. For each rule $r$, let $c(r)$ be the number of premise variables of $r$ that are not yet known to be true. Initially, $c(r)$ is the number of variables in the premise of $r$. For each variable $x \in V$, store the list of rules in whose premise $x$ appears. When $x$ is set to true, scan this list and decrease the corresponding counter by one for each occurrence of $x$ in that premise. If a counter reaches zero, either its rule forces a variable or it forces $\bot$. Before processing variable updates, scan all rules with initial counter value zero. Such rules are exactly those with empty premise: a rule $\top \to y$ immediately forces $y$, while a rule $\top \to \bot$ immediately rejects. After this initialization, the total number of counter decrements is at most the total number of premise literal occurrences in the rule representation, hence at most $N$. Therefore the algorithm runs in time $O(N+n)$ after parsing, including the initial zero-counter scan, and in particular in polynomial time in $N$. [/step] [step:Prove rejection implies unsatisfiability] Suppose the algorithm rejects because a contradiction rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$ has all premise variables true under the current assignment $a$. We prove that $\varphi$ is unsatisfiable. Let $b: V \to \{0,1\}$ be any satisfying assignment of all clauses of $\varphi$, if such an assignment exists. We claim that every variable set to true by the algorithm must also satisfy $b(x)=1$. This is proved by induction over the chronological order in which variables are set to true. If $y$ is set to true by a rule $x_{i_1} \land \cdots \land x_{i_k} \to y$, then all $x_{i_j}$ were previously true under the algorithm. By the induction hypothesis, $b(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$. Since $b$ satisfies the clause corresponding to the implication, the implication forces $b(y)=1$. At rejection time, each $x_{i_j}$ in the premise of the contradiction rule has been set true by the algorithm, hence $b(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$. But then $b$ falsifies the corresponding all-negative clause $\neg x_{i_1} \vee \cdots \vee \neg x_{i_k}$. This contradicts the assumption that $b$ satisfies $\varphi$. Therefore no satisfying assignment exists. [/step] [step:Prove acceptance produces a satisfying assignment] Suppose the algorithm accepts, and let $a: V \to \{0,1\}$ be the final assignment. We verify that $a$ satisfies every clause of $\varphi$. Consider a clause with one positive literal, written as the implication rule $x_{i_1} \land \cdots \land x_{i_k} \to y$. If some premise variable satisfies $a(x_{i_j})=0$, then the implication is true under $a$, so the original clause is satisfied. If instead $a(x_{i_j})=1$ for every $j \in \{1,\dots,k\}$, then the rule is active at the final stage. Since the algorithm stopped only when no active positive rule could force a new variable, we must have $a(y)=1$. Hence the implication, and therefore the original Horn clause, is satisfied. Now consider an all-negative clause, written as the contradiction rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$. If $k=0$, this rule is $\top \to \bot$, which would have fired during the initial zero-counter scan; since the algorithm accepted, this case cannot occur. Hence $k \geq 1$. Because the algorithm accepted, this contradiction rule did not fire at the final stage. Therefore at least one premise variable satisfies $a(x_{i_j})=0$, so the corresponding all-negative clause $\neg x_{i_1} \vee \cdots \vee \neg x_{i_k}$ is true under $a$. Thus every clause of $\varphi$ is satisfied by $a$, so $\varphi$ is satisfiable. [/step] [step:Conclude that Horn-SAT is decidable in polynomial time] The initial syntactic check rejects exactly the inputs that are not well-formed Horn formulas in conjunctive normal form. On the remaining inputs, the forward-chaining algorithm rejects only unsatisfiable Horn formulas and accepts only satisfiable Horn formulas, by the two preceding steps. The syntactic check and the forward-chaining procedure both run in polynomial time in the input length $N$. Therefore the decision problem for satisfiable Horn formulas is decidable by a deterministic polynomial-time algorithm. [guided] We now assemble the full decision procedure. On input $w$, the deterministic parser first checks in polynomial time whether $w$ is a well-formed conjunctive normal form formula and whether each clause is a Horn clause. If either check fails, the algorithm rejects, which is correct for the decision problem under consideration because such an input is not an encoding of a satisfiable Horn formula. Assume now that the input is a Horn formula $\varphi$ with variable set $V := \{x_1,\dots,x_n\}$. The preceding construction rewrites every clause into either a positive implication rule $x_{i_1} \land \cdots \land x_{i_k} \to y$ or a contradiction rule $x_{i_1} \land \cdots \land x_{i_k} \to \bot$, with the empty premise interpreted as $\top$. The forward-chaining algorithm begins from the assignment $a: V \to \{0,1\}$ with $a(x)=0$ for all $x \in V$, repeatedly sets forced conclusions to true, and rejects exactly when a contradiction rule has all its premises true. The runtime is polynomial because each variable changes from $0$ to $1$ at most once. With one counter per rule and one incidence list per variable, every premise occurrence is processed at most once after the initial scan of zero-premise rules. If $N$ denotes the total number of literal occurrences plus the number of clauses, the work after parsing is bounded by $O(N+n)$, hence by a polynomial in the input length. It remains to identify the language decided by the algorithm. If the algorithm rejects, every variable it has forced to true must be true in every satisfying assignment: this follows by induction over the chronological order of forced variables, using the corresponding implication clause at each induction step. Therefore, when a contradiction rule fires, any satisfying assignment would make every premise variable true and would falsify the associated all-negative clause. Thus rejection implies that $\varphi$ is unsatisfiable. Conversely, if the algorithm accepts, no positive rule remains with all premises true and false conclusion, and no contradiction rule has all premises true. Hence every positive Horn clause and every all-negative Horn clause is satisfied by the final assignment $a$. Thus acceptance implies that $\varphi$ is satisfiable. The algorithm therefore accepts exactly the satisfiable Horn formulas and rejects all other inputs, while running in deterministic polynomial time. This is precisely the assertion that Horn-SAT admits a deterministic polynomial-time decision algorithm. [/guided] [/step]