R-Novelty+ SAT heuristic
Algorithms AIMech:RNoveltyPlus DRAFT
Aliases: R-Novelty+
The 1999 R-Novelty extension that replaces its periodic random override with a fixed per-step probability of a random clause-variable flip and otherwise uses the recency- and score-gap-dependent R-Novelty selector.
Identity Notes & Concept Scope
The record is scoped to Hoos’s 1999 R-Novelty+ definition. It removes the original every-100-step override, rather than adding a random-walk branch while silently retaining that schedule. The 2004 competition report uses Rnovelty+ for a periodic configuration; that differently specified variant is not the present identity. At zero walk probability this method reduces to the core R-Novelty selector without the 1997 periodic escape, not the entire original 1997 strategy. 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
3 Claims
Mechanism
#method
Randomly select an unsatisfied clause. With fixed walk probability w in [0,1], choose a variable uniformly from that clause and flip it. Otherwise apply the core R-Novelty selector: rank candidates by global post-flip violation count with oldest-variable tie breaks. Choose the best if it is not the most recently flipped variable in the clause. If it is most recent, let d be the second-best count minus the best count, with d>=1 under the stated age/score assumptions, and use inner noise p in [0,1]. For p<0.5 choose second-best with probability 2p when d=1 and with probability zero when d>1. For p>=0.5 choose second-best with probability one when d=1 and with probability 2(p−0.5) when d>1. Choose best otherwise. Update the timestamp of the flipped variable. Omit the periodic every-100-step override: the new walk coin is evaluated at each step. A fixed w>0 supports the source’s asymptotic result; w=1 gives pure clause-first random walk and w=0 retains only the core selector.
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.
Scope
#plus-source-version-boundary
Hoos1999 explicitly removes the periodic escape when defining R-Novelty+, while the 2004 competition report calls an every-100-step configuration Rnovelty+. This record follows the former definition and does not treat the latter’s cycling-prevention statement as its theorem.
⚠️ 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.
- The asymptotic guarantee for the 1999 per-step extension must not be transferred to the 2004 periodic configuration merely because both use a plus label. The previously proved trapping example shows why scheduled random steps can miss an essential variable.
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
3 Sources| Source ID | Publication / Document | Type / Access | Reference & Checksum |
|---|---|---|---|
method-source
|
Holger H. Hoos
|
primary paper
full_text
|
sha256:6afd11724464…
|
additional-1
|
David McAllester, Bart Selman, Henry Kautz
|
primary paper
full_text
|
sha256:79821a112c8c…
|
additional-2
|
Henry Kautz, Bart Selman, David McAllester
|
author technical report
full_text
|
sha256:525f46d2f9fd…
|
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/RNoveltyPlus.yaml