Tabu search for SAT (TSAT)

⚠️ Curated Limitations & Negative Results

• The 1997 presentation does not supply a complete dedicated TSAT pseudocode. Initialization and reset of tabu memory, ties, the discrete tenure boundary and empty-admissible-set behavior need explicit operational conventions. Figure 3 is basic GSAT; later implementation choices must not be silently substituted for the original account.
• A declared integer tenure and variable universe are needed. For n>0 variables and a tabu set of at most T distinct variables, 0≤T<n ensures that some variable is admissible. If T≥n, all variables can become tabu without an intervening reset. The inspected paper gives no general all-tabu fallback or aspiration escape; a fitted fractional tenure also needs an integer convention.
• Finite unsuccessful search is not an UNSAT certificate, and recent-variable exclusion does not prove global cycle freedom or eventual success. On the unsatisfiable conjunction of all four two-variable clauses, every flip has zero gain; tenure one can permit alternating x,y flips that revisit an assignment after four steps and an augmented assignment/list state after the fifth, absent an intervening cutoff or reset. This is a hand boundary example, not an observed run.
• The best admissible flip need not improve the clause score, and a useful move can be tabu. No-aspiration TSAT differs from tabu configurations with aspiration, adaptive tenure or longer-term intensification and diversification. Constant-time circular FIFO access does not establish constant-time evaluation of all flips or constant-time search.
• The displayed linear formula for an experimentally best tabu-list length is a fit for the reported random K-SAT studies, not a universal optimum, theorem, rounding rule or guarantee for structured SAT. The paper identifies dynamic lengths and structured examples as further work; no fixed tenure is mandated here for every problem.
• Table 1 reports time and flip averages on solved instances, with solved percentages relative to an approximately 50% expected satisfiable subset at the phase transition. These denominators and the common C/Linux/Pentium platform, budgets and tested distributions limit interpretation. The comparisons do not establish universal speedups, exact satisfiable-instance success rates or whole-solver complexity, and no benchmark was reproduced.
• The CP95 reference, the 1997 paper and later GSAT/TABU documentation remain distinct versions. The inspected UBCSAT selector has no explicit zero-candidate branch before reading candidate index zero; complete infrastructure and runtime behavior were not audited, so no observed implementation failure is asserted. The earlier timid TSAT and the clause-focused WalkSAT/TABU/null-move variants are not aliases of this scoped method.