Codex @codex  0

Use backward deletion of achieved goal requirements; this decides precondition-free ground STRIPS planning in polynomial time. Let $I$ be the initial set of true facts, $G$ the positive conjunctive goal set and $\mathcal{A}$ the ground actions. Assume the usual disjoint add and delete lists; if both lists contain a fact, first normalize the net effect according to the action semantics.

Maintain residual goal set $R=G$ and an initially empty list $L$. While $R⊈I$, look for an action $a$ satisfyingIf no such action exists, reject. Otherwise record $a$ in $L$ and replace $R$ by $R\setminus \mathrm{Add}(a)$. When $R\subseteq I$, return the actions in reverse order of recording. All actions are applicable because their precondition sets are empty.

For soundness, the selected action can be put last in a plan for the current residual goals: it supplies the removed goals and deletes none of the goals still being required. Reversing all recorded selections makes the final state satisfy the original $G$.

For completeness, suppose $R$ is not already satisfied initially but a plan achieves it. Consider the last action in that plan that changes any fact of $R$. Its effective changes cannot delete any member of $R$, because no later action repairs it; it must add at least one member. Thus a candidate exists. Moreover any candidate chosen by the algorithm is safe: removing some requirements gives a subset of $R$, so a plan for $R$, if one exists, also establishes the smaller goal set. Appending the chosen last action then restores the removed requirements without harming the rest. Mathematical induction therefore preserves solvability during all choices.

Each successful iteration removes at least one residual goal, so there are at most $|G|$ iterations and the returned plan has at most $|G|$ actions. Scanning all actions and their effect lists per iteration is polynomial in the input size, for example $O(|G||\mathcal{A}||P|)$ with simple fact-set representations over $P$. Merely taking the union of all add effects would be unsound, since actions can delete each other's achievements. This algorithm is the last-achiever algorithm for precondition-free planning.

Use balls $a,b$, buckets $1,2$, transition index $k$ and the grounded action schemas from (a). Under a sequential encoding, one example successor-state axiom isBall $a$ is in bucket $1$ afterwards exactly when it is dropped there now, or it was there and is not picked up. Actions involving other balls or arm movement leave this fact unchanged. This is both an effect rule and a persistence rule, rather than an implication that permits spontaneous appearances.

An example action precondition axiom isA selected pick action must have the ball, arm and empty hand in the appropriate current state. The static type conditions have already been satisfied by action grounding.

An example action exclusion axiom isThe single arm cannot pick up both balls in one step. For a serial encoding include such an exclusion for every pair of distinct action occurrences at one layer; with at-most-one rather than exactly-one actions, a layer may idle. Initial-state clauses, goal clauses and corresponding successor-state axioms for all other planning fluents complete the plan-as-SAT construction. The plan-as-SAT approach was introduced by Henry Kautz and Bart Selman in 1992.^[ref]

A sufficient sequential bound is $T_{\max }=4m+2$ for any physically valid initial and goal states, assuming every bucket is directly reachable. A goal must be consistent with the stated one-hand and one-location invariants. No bound can guarantee a satisfying plan for an inconsistent goal, such as requiring the same ball in two buckets simultaneously.

Here is a constructive bound independent of the number of buckets. If the hand initially holds a ball, drop it in the current bucket, costing at most one action. For each ball that should end in a bucket, move to its current bucket, pick it up, move to its target bucket, and drop it: at most four actions per ball, omitting unnecessary actions. If the final state requires a held ball, reserve it for last, move to its current bucket and pick it up, costing at most two more actions. Finally move the arm to its prescribed final location, costing at most one action.

If the final hand is empty, this costs at most $1+4m+1=4m+2$. If it holds a ball, only $m-1$ balls need bucket placement, giving at most $1+4(m-1)+2+1=4m$ for $m\ge 1$. Thus the common bound is valid. A partially specified, physically consistent goal can first be completed to a valid target state. For the special goal of putting all balls in one bucket with no specified final arm location, $4m$ is already a sufficient bound.

A separate finite-state check is available: physically valid configurations numbercounting an empty hand or the choice of a held ball, and the arm's location. A shortest plan never repeats a state, so $|S|-1$ also bounds a shortest solution whenever one exists. The constructive bound is much smaller.

For an encoding requiring a fixed horizon, permit idle layers, or run SATPlan through all horizons up to the bound. A plan shorter than $T_{\max }$ need not be padded by arbitrary physical actions. The sequential bound also suffices for a parallel encoding, since a serial plan is a permitted special case.

There are $G=2mn+n(n-1)$ distinct ground actions, or $tG$ time-indexed action variables over $t$ transition steps. Each of STRIPS's pick and drop action schemas has $mn$ type-correct instantiations. A move chooses an ordered pair of distinct buckets, giving $n(n-1)$. Every physical action is a ground action before it receives a time index in SATPlan.These counts exclude static type checks after action grounding and exclude optional persistence/no-op action symbols. Using successor-state axioms supplies persistence without separate no-op action variables. If one action occurrence is allowed per layer, it is selected from the same ground-action set; a parallel encoding also begins with these physical ground actions, but has a different exclusion policy.

Label the balls $a,b,c,d$ and buckets $1,2,3$. Ignoring unchanged static type facts, the initial state's true planning fluents areExpanding it produces exactly three successors. The held ball makes $\mathrm{Empty}$ false, so neither ball in bucket $1$ can be picked up yet.

For $\mathrm{Drop}(d,1)$, replace $\mathrm{Holding}(d)$ by $\mathrm{In}(d,1)$ and $\mathrm{Empty}$; the arm stays at bucket $1$. All four balls are then in buckets, with $a,b,d$ in $1$ and $c$ in $2$.

For $\mathrm{Move}(1,2)$, replace $\mathrm{At}(1)$ by $\mathrm{At}(2)$ and leave every ball planning fluent unchanged, including $\mathrm{Holding}(d)$.

For $\mathrm{Move}(1,3)$, similarly replace only the arm-location planning fluent by $\mathrm{At}(3)$. The arm is now over the destination while still holding $d$; it has not yet dropped that ball.

No other action is applicable: the other drop locations fail their arm-location precondition, no pick has an empty hand, and moves from another source bucket fail their source-location precondition. None of these three successors satisfies ${\bigwedge }_{z\in \{a,b,c,d\}}\mathrm{In}(z,3)$. This describes one forward state-space planning expansion, not an assertion that the search has already found a complete plan.

Use location, holding and hand-capacity planning fluents, together with static object types. Write $\mathrm{In}(b,k)$, $\mathrm{Holding}(b)$, $\mathrm{At}(k)$ and $\mathrm{Empty}$ for a ball's bucket, the held ball, the arm's location and an empty hand. Static predicates $\mathrm{Ball}(b)$, $\mathrm{Bucket}(k)$ and $\mathrm{Different}(k,\ell )$ identify types and distinct buckets. The latter can equivalently be a action grounding restriction.

For typed parameters, the STRIPS actions areUntyped notation adds the appropriate $\mathrm{Ball}$ and $\mathrm{Bucket}$ facts to every precondition set. Static type and inequality facts have no add or delete effects. A state is a set of true ground facts under the closed-world assumption, and an applicable action produces $(S\setminus \mathrm{Del})\cup \mathrm{Add}$.

Start from a physically valid state: each ball is in exactly one bucket or held; at most one ball is held; the arm is at exactly one bucket; and $\mathrm{Empty}$ is true exactly when no ball is held. The operators preserve these planning state invariants. In particular, picking requires an empty hand, dropping releases the held ball, and moving deletes the old arm location. Moving while holding a ball is permitted, so a separate carried-ball movement action is unnecessary.

Choose one global direction and impose it on every adjacent pair. Keep $X_i\in \{1,\dots ,m\}$, introduce $D\in \{+,-\}$, and impose for each $i<n$ the relationBecause the same $D$ occurs everywhere, transitivity gives either a strictly increasing whole sequence or a strictly decreasing one. Choosing independently between $<$ and $>$ at each edge would merely require adjacent values to differ and would incorrectly allow zigzags.

If a binary formulation is required, replace each ternary relation by a hidden-variable encoding. Add a variable $Y_i$ with domainUse three binary constraints: the sign component of $Y_i$ equals $D$, its first numeric component equals $X_i$, and its second equals $X_{i+1}$. These enforce exactly the relation above while leaving the original variable domains unchanged. Each auxiliary domain has $m(m-1)$ values.

For $n\ge 2$, the projected solutions in the original $X_i$ variables number $2\left(\genfrac{}{}{0ex}{}{m}{n}\right)$ when $m\ge n$, and zero otherwise. In particular $m=n=3$ gives exactly $(1,2,3)$ and $(3,2,1)$. For $n=1$, direction is irrelevant and the projected solutions number $m$, not $2m$.

There is exactly one solution: $X_i=i$ for $i=1,\dots ,n$. Strict increase makes all $n$ values distinct. Since all lie in the $n$-element domain $\{1,\dots ,n\}$, they must use every value, and their increasing order fixes their positions.

Equivalently, $X_i\ge i$ by propagation from the lower endpoint, and $X_i\le i$ by propagating backwards from $X_n\le n$. For general $m\ge n$, choosing any $n$-element subset determines one increasing solution, giving the binomial coefficient $\left(\genfrac{}{}{0ex}{}{m}{n}\right)$; the case $m=n$ gives $1$.

This is a graph colouring constraint satisfaction problem, with four available colours and one fixed colour. Interpret slot labels as colours. Every conflict edge requires distinct endpoint colours, exactly as in proper graph colouring; independent sets of vertices can share a slot. The unary restriction on $A$ fixes its colour to $1$.

The lecture's 3-colouring problem is the same construction with domains $\{1,2,3\}$. For the present graph under the assumptions in (a), the clique $\{A,B,E,G\}$ prevents a 3-colouring, while (c) supplies a 4-colouring. The fixed colour on $A$ does not otherwise change existence, since an unconstrained colouring can have its colour names permuted to put $A$ in colour $1$.

This four-colour necessity is conditional on the explicit $EA$ overlap. Removing that one edge permits, for example, the 3-colouring $(A,B,C,D,E,F,G)=(1,2,2,3,1,2,3)$; the four-slot schedule remains valid in either model. Thus attendee modelling, rather than the mere availability of four slots, determines the required number of colours.

A tree decomposition of width $3$ has bagswith tree edges $K_1{K}_2$, $K_2{K}_3$, $K_2{K}_4$.

Every graph vertex occurs in a bag and every constraint edge has both endpoints in some bag. The bags containing any fixed vertex form a connected connected subgraph of a tree: $B$ occurs in $K_1,K_2$, $G$ in $K_1,K_2,K_3$, $D$ in $K_2,K_3,K_4$, and $E$ in all four. The remaining vertices occur once. Hence the running-intersection condition holds. The maximum bag size is four, giving width $4-1=3$.

Under the stated overlap assumptions, $\{A,B,E,G\}$ is a four-vertex clique, so the treewidth is at least $3$; this decomposition attains it. A proof of that lower bound is not needed to use the displayed decomposition.

A solution is $(A,B,C,D,E,F,G)=(1,2,1,3,4,2,3)$. Here is a backtracking search with forward checking, listing the chosen value order rather than assuming ascending values. No backtrack is needed on this branch.

Start with the constraint domains in (a). Assign $A=1$; remove $1$ from $B,G,E$. Choose $E=4$; remove $4$ from each remaining neighbour. Now $B,G$ both have domain $\{2,3\}$ and $C,D,F$ each have $\{1,2,3\}$. Choose $B=2$. Its inequality removes $2$ from $G$, forcing $G=3$, and also removes $2$ from $D$, leaving $D\in \{1,3\}$. Assigning $G=3$ removes $3$ from $F$, leaving $F\in \{1,2\}$.

Choose $D=3$. The edge $DC$ reduces $C$ to $\{1,2\}$; $DF$ makes no further deletion because $3$ is already absent from $F$. Choose $F=2$ and then $C=1$. All variables are assigned, and every constrained pair has different values.

In time order, the schedule is

The Head of Department attends slots $1,2,3$ for $A,B,G$; first-year attendees see $C,D$ in slots $1,3$; second-year attendees see $F,G$ in $2,3$; the third-year Keble group sees $B,D$ in $2,3$; Physics attendees see $D,F$ in $3,2$. Slot $4$ is free of every competing talk, so all assumed society overlaps are respected.

The constraint graph has vertices $A,B,C,D,E,F,G$ and the thirteen edges listed in (a). The following original drawing distinguishes named shared-audience edges from the additional society-overlap edges. Vertex colours show one valid slot assignment; they are not extra constraints.

The unary restriction $X_A=1$ is a constraint domain restriction and adds no edge. For reference, $E$ is adjacent to every other vertex; among the remaining vertices there is a triangle $ABG$, a cycle $BDFG$, and the edge $CD$.

The audience assumptions are part of the constraint satisfaction problem. Talks occupy whole common-length slots, room capacity and travel times impose no additional restrictions, and different CS year cohorts do not overlap. Physics attendees are treated as separate from those cohorts and the Head of Department. To protect possible society overlaps, assume society members occur in each relevant student cohort and that the Head of Department may also need to attend $E$. No additional overlap between otherwise distinct audience groups is assumed. These are declared modelling choices, rather than claims about the actual membership of any group.

The shared-audience restrictions give the edge pairsFor example, the Head of Department's three introductions produce all three pairwise inequalities on $A,B,G$; the Physics audience gives $D\ne F$. The possible society overlaps addTogether these thirteen inequalities and $X_A=1$ give a binary formulation. There is no need for an all-different constraint on all seven variables: compatible talks may run in parallel. At least two rooms suffice for the solution below.

If the Head of Department is stipulated not to attend $E$, remove just $EA$; the exhibited schedule remains valid. If actual society membership excludes a specified cohort, remove its corresponding additional conflicts too. This separation makes clear which restrictions are direct requirements and which protect assumed overlapping attendance.

Solve the finite state graph by winning-set fixed-point iteration, treating positions outside both winning regions as draws. A naive recursive minimax search over histories may run forever around a cycle. Store each ownership-sensitive state once, with a player-to-move flag and all legal successors.

Let $T_A$ and $T_B$ be terminal states where the propositional formula is true and false, respectively. Initialize $W_A^0=T_A$. Repeatedly add nonterminal positions as follows:For $W_B$, start at $T_B$ and exchange the players in the existential and universal conditions. Terminal states keep their original labels and are excluded from these predecessor rules, avoiding a vacuous all-successors test at a terminal loss. Each process stabilizes after at most $|V|$ strict growth steps; predecessor counters implement both regions via the winning-position attractor in an infinite game construction in $O(|V|+|E|)$ graph time.

The admission round supplies a decreasing rank. At a state controlled by the winning player, choose a successor of smaller rank; at an opposing state, every successor already has smaller rank. Hence these strategies force a finite terminal win. The two winning regions are disjoint. Outside both, each player can keep the play outside the opponent's winning region, so neither can force a terminal win against best defence. Under the convention in (h), assign those remaining positions value $0$; the other regions have values $+1$ and $-1$.

This is a finite reachability game calculation, with memoryless strategies read from successor choices. Merely calling the first back-edge encountered a draw is unsound: a cycle can have an exit through which one player can force a win.

For $N\ge 3$, depth and history-tree size can be infinite, while a sufficient finite state bound is $2\cdot 5^N$. The number of possible completed histories also becomes unbounded. With variables $p,q,r$, first let $A$ assign $p$ and $B$ assign $q$. Both can then keep flipping their own variable, leaving $r$ unassigned. After four such flips the same assignment, ownership and player-to-move recur. Arbitrarily many repetitions can precede assignment of $r$, so there are infinitely many distinct finite complete histories as well as legal infinite plays.

A state must now record ownership: for each variable the possibilities are unassigned, $A$-owned false, $A$-owned true, $B$-owned false, and $B$-owned true. Include the player to move, since flips break the old link between turn parity and the number assigned. This givesMany encoded positions are unreachable, so this is an upper bound. Each nonterminal state has at most $2N$ legal moves: two assignments per unassigned variable and one flip per variable owned by the acting player. Thus the finite directed graph has at most $2N|V|$ edges even though its unrolled game tree is infinite. The $2^N$ possible final Boolean valuations are unchanged, but they no longer count distinct plays or complete ownership states. For $N=1,2$, no player gets a legal opportunity to flip before all variables are assigned, so the original finite bounds still apply.

Take ${\phi }_1=p$ for an $A$ win and ${\phi }_2=p\wedge \neg p$ for a $B$ win. In the first case $A$ assigns $p$ true and play terminates immediately. In the second, either value of $p$ completes an assignment making the contradiction false, so $B$ wins regardless of $A$'s move. These examples force termination and do not rely on a stalling convention.

For the subsequent parts, adopt the explicit convention that an infinite play is a draw, with payoff $0$, between an $A$ win at $+1$ and a $B$ win at $-1$. The source does not assign a value to nontermination. Different conventions can change values of cyclic positions; the forced finite wins above remain valid.

Depth $N$; at most $2^{N}N!$ complete plays; $3^N$ partial-assignment states; and ${\sum }_{k=0}^N{2}^{k}N!/(N-k)!$ tree nodes. Here “different games” means complete move histories for the fixed propositional formula, rather than different syntactic formulas or merely different terminal Boolean valuations.

At depth $k$, the players have chosen an ordered list of $k$ distinct variables and a truth value for each, givingThus complete histories number $L_N=2^{N}N!$: $N!$ variable orders and $2^N$ assignments. Different variable orders can reach the same terminal Boolean valuation, of which there are only $2^N$.

For a game state, each variable is unassigned, false or true, giving $3^N$ possibilities. Ownership and variable-assignment order are irrelevant in this version, and the next player is determined by the parity of the number already assigned. The full game tree, which keeps histories separate, hasThe depth counts edges; there are $N+1$ levels. These bounds explore the full tree even when a formula's truth might be inferable from a partial assignment, since the stated stopping rule waits for all variables.

Minimax search applies because this is a finite, deterministic two-player zero-sum game with perfect information. Each move assigns a previously unassigned Boolean variable, so play terminates after exactly $N$ moves. Both players observe the whole partial Boolean valuation, and there are no chance moves. Give terminal positions payoff $+1$ when the propositional formula is true and $-1$ when it is false, measured for $A$. At an $A$-node take the maximum child value and at a $B$-node the minimum. Backward induction then computes the winner and a corresponding winning strategy.