Home / Curated / Algorithms / Novelty+ SAT heuristic

Novelty+ SAT heuristic

Algorithms AIMech:NoveltyPlus DRAFT

Aliases: Novelty+

A Novelty extension that, at each SAT search step, chooses a random variable from a randomly selected unsatisfied clause with a fixed walk probability and otherwise uses Novelty’s recency-conditioned best/second-best selector.

Identity Notes & Concept Scope This is Hoos’s 1999 Novelty+ random-walk extension. The plus sign identifies an additional per-step random-walk branch, distinct from Novelty’s conditional noise parameter and from later adaptive, diversification or look-ahead variants. It does not require a periodic schedule or an SKC zero-break priority. The theorem concerns asymptotic model finding on satisfiable formulas, not probably-approximately-correct learning or a finite UNSAT decision. No normalized identity match was found across all 442 pinned AIO labels/scoped synonyms and 325 preceding native IDs/names/aliases. Full-checkout fixed-string searches included ignored and hidden files in worktree and main, returning 90 and 90 lines respectively. All 64 unique hit contents were inspected: neighboring variant and source references, saved reviews and candidate leads, not existing candidate records. Exact checkout counts and differences are retained in the ledger. Nine exact AIO CLASS nodes with scoped synonyms/comments and outgoing edges and five full native neighboring records were inspected. Absence is bounded to this snapshot and semantic neighborhood.

Claims & Grounded Evidence

2 Claims

Mechanism #method

Maintain a complete truth assignment and variable flip timestamps. If the formula is not satisfied, randomly choose an unsatisfied clause. With fixed probability w in [0,1], choose a variable uniformly from that clause and flip it. Otherwise rank clause variables by the global post-flip violation count, breaking score ties in favor of the least recently flipped variable. If the best is not the most recently flipped variable in the clause, select it; otherwise select second-best with probability p and best with probability 1−p, where p is in [0,1]. Update the flipped variable’s timestamp and continue under the declared stopping policy. The walk branch is available regardless of scores, recency or zero-break candidates. With w=1 this is the pure clause-first random walk; with w=0 it is the underlying Novelty selector. Any fixed w>0 satisfies the source’s random-walk premise once all remaining move cases are well-defined.

supports Source: On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT · Locator: PDF5–6, Improving SLS Performance, per-step random-walk extension and naming; PDF2, WalkSAT/Novelty context; PDF3–4, asymptotic scope and Theorem 2
supports Source: Evidence for Invariants in Local Search · Locator: PDF2 / printed322, Novelty and R-Novelty selector definitions; PDF3 / printed323, original periodic R-Novelty override

Scope #asymptotic-model-finding

For a finite satisfiable CNF and a well-defined remaining move policy, a fixed positive lower bound on the probability of a uniform random-clause/random-variable step at every search step gives success probability approaching one as the number of steps tends to infinity. Hoos1999 Theorem 2 establishes this via a positive probability of a sequence reducing Hamming distance to a model. The conclusion does not give a polynomial or practically small runtime, a finite-run guarantee, or an UNSAT certificate.

supports Source: On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT · Locator: PDF3, Definition 2 and no-restart scope; PDF3–4, Lemma 1 and Theorem 2; PDF5–6, application to the plus extensions

⚠️ Curated Limitations & Negative Results

The asymptotic guarantee requires a strictly positive walk probability at every step, bounded below independently of elapsed search history. A scheduled-only override or a probability that tends to zero does not automatically satisfy that premise. At w=0 the random-walk argument no longer applies.
The guarantee concerns finding a model on a finite satisfiable formula in the limit of continued search. A finite budget can miss an existing model and cannot certify UNSAT. The source’s lower bound can be extremely small; no polynomial or practical runtime follows.
The walk probability w is separate from the inner selector’s noise parameter p. The reported experimental w=0.01 is not a defining or universally optimal constant. Optional outer restarts and cutoffs must be specified separately.
Empty clauses, unit clauses lacking a second candidate, initial age ties, duplicate literals and timestamp/reset conventions require a well-defined implementation. The general random-walk proof does not certify undocumented choices in the short selector description. No author solver or benchmark was executed.

Artificial Intelligence Ontology (AIO) Grounding

Explicit AIO Snapshot Assessment: No Match

Rationale: No suitable AIO target was established in the pinned snapshot and inspected SAT/search/memory neighborhood. A positive random-walk probability and variable-age bookkeeping do not justify forced neural-memory, language-model or learning-task mappings.

Search Scope: All 442 pinned AIO labels/scoped synonyms and 325 preceding maintained IDs/names/aliases; ignored/hidden-inclusive full text in both checkouts; semantic labels/scoped synonyms for search, satisfiability, heuristics, reasoning, novelty, memory and recurrence; nine exact AIO CLASS nodes and five complete native neighbors.

Examined AIO Candidate	Rejection Reason
`AIO:ReasoningLLM`	Selecting Boolean variable flips is not a language model performing reasoning in language tasks.
`AIO:TrainingStrategy`	The method searches a supplied formula rather than prescribing preprocessing or training a machine-learning model.
`AIO:MachineLearningTask`	Remembering a move timestamp does not itself turn fixed-formula search into development of a method that learns from data.
`AIO:ReinforcementLearning`	Age-based move selection and a noise parameter do not require a learned reward policy or action-value function.
`AIO:MarkovChain`	An augmented state could include timestamps and step phase, but that representation alone does not identify the named SAT heuristic with the pinned stochastic network/model class.
`AIO:ArtificialNeuralNetwork`	Boolean assignments, clause scores and flip timestamps are not a network of artificial neurons.
`AIO:MemoryAugmentedLLM`	External memory in a language model is different from retaining SAT variable ages; the related external-memory synonym does not broaden the target to every algorithm using memory.
`AIO:MemoryCellLayer`	A neural layer of cells with internal state or weights is not a variable-age table.
`AIO:LongShortTermMemory`	A recurrent neural architecture processing sequences is not a SAT move-history heuristic.

Evidence Sources & Primary Literature

2 Sources

Source ID	Publication / Document	Type / Access	Reference & Checksum
`method-source`	On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT Holger H. Hoos	primary paper full_text	sha256:6afd11724464…
`additional-1`	Evidence for Invariants in Local Search David McAllester, Bart Selman, Henry Kautz	primary paper full_text	sha256:79821a112c8c…

Curation Provenance

Curator: Codex

Method: ai_assisted

Model: GPT-6

Created: 2026-10-11T15:57:02Z

Updated: 2026-10-11T15:57:02Z

Source File: data/curated/NoveltyPlus.yaml