R-Novelty SAT heuristic
Algorithms AIMech:RNovelty DRAFT
Aliases: R-Novelty
A Novelty-derived SAT heuristic whose choice between the best and second-best flips depends on their objective-score gap when the best variable was most recently flipped; its original 1997 search strategy also includes a periodic random clause-variable move.
Identity Notes & Concept Scope
This record follows the full 1997 R-Novelty parameterization and its stated every-100-flip random override, retaining the distinction from the core score-gap selector and from the 1999 R-Novelty+ extension. The 2004 solver description instead labels a periodic-override configuration Rnovelty+ and describes only the p=0.5 selector case. Those differing source conventions are not treated as exact synonyms or interchangeable completeness guarantees. No normalized identity match was found across all 442 pinned AIO labels/scoped synonyms and 322 preceding native IDs/names/aliases. Full-checkout fixed-string searches included ignored and hidden files in worktree and main, returning 52 and 53 lines respectively. All twenty unique hit contents were inspected: neighboring variant references, saved reviews and discovery leads, generic novelty wording and an ignored Sphinx comment, not existing candidate records. The checkout 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
Use Novelty’s randomly selected unsatisfied clause, post-flip total-violation ranking and oldest-variable tie break. If the best candidate is not the most recently flipped variable in that clause, select it. Otherwise let d be the second-best post-flip violation count minus the best count; the 1997 rule assumes d>=1. If p<0.5 and d>1, choose the best. If p<0.5 and d=1, choose the second-best with probability 2p and otherwise the best. If p>=0.5 and d=1, choose the second-best. If p>=0.5 and d>1, choose the second-best with probability 2(p−0.5) and otherwise the best. Independently of this ordinary selection rule, the 1997 strategy specifies that every 100 flips it chooses a random variable from the selected clause instead. Update the chosen variable’s flip timestamp. At p=0.5 the recency-triggered rule picks second-best for gap one and best for a larger gap; that special case is not the full parameterized method.
Scope
#incompleteness-and-version-boundary
Hoos1999 proves essential incompleteness of unrestarted R-Novelty even with scheduled random flips every 100 steps, then defines R-Novelty+ by replacing that periodic escape with a positive per-step random-walk branch. The 2004 competition report uses the plus name for a periodic configuration and claims cycling prevention. This record preserves the discrepancy and follows the explicit 1997 method and 1999 theorem, without endorsing the conflicting guarantee.
⚠️ Curated Limitations & Negative Results
- Hoos1999 Theorem 4 and its continuation show that the unrestarted R-Novelty strategy is essentially incomplete for arbitrary noise settings even with its every-100-step override. A periodic random move can occur at phases that never expose a needed variable; its mere presence does not establish asymptotic success.
- The 1999 R-Novelty+ method removes the periodic override and adds a positive random-walk probability at each step. Its guarantee relies on possible arbitrarily long random-walk sequences, not a deterministic schedule. The 2004 source uses the plus name differently and its cycling-prevention statement is not adopted as a guarantee.
- The d>=1 branch formulation uses age-based score tie breaking. Initial timestamp ties, unit clauses with no second candidate, empty clauses and exact counter/reset conventions need explicit implementation decisions; a d=0 probability rule is not invented here.
- Parameters p and the periodic schedule have different roles. Score gaps are in unweighted clause counts; changing them to weighted or real-valued objectives requires a new specification. Finite failure is not an UNSAT proof, and 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 this pinned snapshot and inspected semantic neighborhood. Search memory, novelty naming and stochastic exploration do not justify forced neural-memory, language-model or learning-task mappings.
Search Scope: All 442 pinned AIO labels/scoped synonyms and 322 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
|
David McAllester, Bart Selman, Henry Kautz
|
primary paper
full_text
|
sha256:79821a112c8c…
|
additional-1
|
Holger H. Hoos
|
primary paper
full_text
|
sha256:eb69383aef4a…
|
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:45:43Z
Updated: 2026-10-11T15:45:43Z
Source File:
data/curated/RNovelty.yaml