Home / Curated / Algorithms / HRSAT

HRSAT

Algorithms AIMech:HRSAT DRAFT

A source-scoped SAT-search algorithm described by the literal composition of the 1995 GenSAT stages: a probability-controlled choice between false-clause variables and globally best-scoring flips, followed by HSAT’s least-recently-flipped selector. The paper’s generic random-walk prose does not uniquely certify this composition as its experimental executable.

Identity Notes & Concept Scope Gent and Walsh1995 Figure1 defines the source-scoped HRSAT candidate-pool coin followed by history selection in either pool. The accompanying prose wording is retained as an ambiguity. Later UBCSAT1.0.0 HWSAT uses a clause-first uniform random variable rule and is comparative evidence, not an exact alias. Existing HSAT, IHSAT, GSAT-with-random-walk, WalkSAT and AutoWalksat have distinct pool, picking or outer-controller scopes. At clean merged base14e9168ee3496e914545ae5c449e3ee190f0294b, the current inventory has786 native and442 pinned AIO records:4876 identity-field occurrences,3723 normalized values, and no candidate collision. Four full-checkout searches included ignored and hidden files; all1329 distinct matching contents (23381 occurrences) were read by the attributed root/team partitions, with18 contextual fields across ten neighboring records assessed separately. This is bounded identity evidence, not proof of universal semantic absence.

Claims & Grounded Evidence

5 Claims

Mechanism #printed-gensat-search-context

In the inspected 1995 GenSAT framework, begin an attempt from an initialized complete Boolean assignment; the GSAT initialization described in Section 2 is random. Before each permitted flip, test whether the assignment satisfies the CNF formula. Otherwise select a candidate set, pick one variable, flip its truth value and continue within the per-attempt flip budget and outer attempt budget. HRSAT is introduced as a variant within this framework.

supports Source: Unsatisfied Variables in Local Search · Locator: PDF pp. 2–4, Section 2, Figure 1 and Section 4 introducing HRSAT.

Mechanism #probability-controlled-candidate-set

In the literal printed select stage, choose with probability p the set of all variables occurring in currently unsatisfied clauses. With probability 1−p, choose the variables whose single-variable flips give the greatest change toward more satisfied clauses, as in the stated GSAT hclimb rule. A greatest change need not be positive. The focused branch is available even when an improving flip exists; Section 5.3 treats allowing walks only when hill climbing is unavailable as a separate variant.

supports Source: Unsatisfied Variables in Local Search · Locator: PDF pp. 2–3, Section 2 and Figure 1; PDF p. 8, Section 5.3, the separately restricted walk variant.

Mechanism #literal-history-pick-composition

After select returns its candidate set, the printed driver applies pick to that set. For HRSAT, compose this with the HSAT strategy described in Section 4: choose a candidate whose last flip was longest ago. The same section explicitly contrasts this history-based deterministic picking with random picking. This is a source-scoped reading of the printed stages, not a claim that the paper’s generic random-walk prose fully specifies or certifies the experimental implementation.

supports Source: Unsatisfied Variables in Local Search · Locator: PDF p. 3, Figure 1 and HSAT pick definition in Section 4; PDF pp. 4–5, HRSAT introduction and deterministic/history-picking discussion; PDF p. 8, generic random-picking prose retained as a qualification.

Mechanism #focused-moves-and-endpoints

A focused flip changes a variable appearing in a false clause and can reduce the total number of satisfied clauses. Under the literal composition and the same history, tie and outer-loop conventions, p=0 recovers the HSAT candidate/pick combination, while p=1 always uses the false-clause variable pool but retains the history selector. The latter endpoint is not a uniform random draw from that pool or a clause-first random walk.

supports Source: Unsatisfied Variables in Local Search · Locator: PDF pp. 1–3, discussion of downward focused flips, Section 2 and Figure 1; PDF pp. 3–5, history picking. Endpoint statements are direct consequences of the stated probability branch and composition.

Scope #archived-hwsat-version-distinction

The inspected UBCSAT 1.0.0 archive registers HWSAT as HSAT with random walk and cites the Gent–Walsh paper. Its unweighted PickHWSat walk branch instead chooses an unsatisfied clause uniformly and then a literal uniformly from that clause, flipping the corresponding variable; its other branch delegates to PickHSat. This is a separately versioned implementation policy, not evidence that HWSAT is an exact alias of the literal HRSAT composition curated here.

supports Source: UBCSAT 1.0.0 source archive: HWSAT selector in src/hwsat.c · Locator: Archive member src/hwsat.c, AddHWSat lines 28–41 and unweighted PickHWSat lines 56–77. The explicit uniform clause/literal comment accompanies the two RandomInt selections.
supports Source: Unsatisfied Variables in Local Search · Locator: PDF p. 3, Figure 1; PDF pp. 3–5, HRSAT history selector, for the original composition being contrasted.

⚠️ Curated Limitations & Negative Results

The 1995 printed select/pick stages and deterministic-history discussion support this literal composition, while the paper also uses generic random-walk and random-picking prose. This record preserves that ambiguity; it does not claim to reconstruct the exact experimental executable or silently substitute a uniform focused selector.
The later HWSAT name does not establish identical transition rules. The inspected UBCSAT 1.0 clause-first sampling differs from both history picking over the full focused pool and uniform sampling of the duplicate-free variable union. The complete delegated HSAT helper, solver infrastructure and later releases are not certified by this comparison.
The 1995 summary does not restate every initialization, never-flipped tie and restart convention from the earlier HSAT work. Those choices must be specified for an operational implementation; no convention is imported here from a maintained neighbor as though it were fresh primary evidence. A history preference is not a tabu-tenure exclusion.
The probability parameter lies in [0,1], and a focused flip needs an eligible variable. Empty clauses or an empty eligible set require explicit handling outside that selector. Clause/literal multiplicity and normalization can alter score counts or clause-first sampling; representation choices are not silently standardized.
Finite unsuccessful search is not an UNSAT certificate. Figure 1 tests satisfaction before each flip, so a model reached on the final permitted flip is not rechecked inside that literal loop. An added final test must be declared rather than treated as printed behavior.
The reported parameter studies and random/structured benchmarks do not establish a universal p, restart budget, speedup or asymptotic complexity bound. Difficult structured examples and the dependence on encoding and parameter choices remain within the source’s scope. No solver or benchmark was executed for this record.
Focused moves need not improve the score, and the history selector does not give every eligible variable a positive uniform probability at each step. General random-walk or 2-SAT convergence bounds therefore do not automatically apply. Endpoint agreement at p=0 does not identify the full parameterized method with ordinary HSAT.

Artificial Intelligence Ontology (AIO) Grounding

Explicit AIO Snapshot Assessment: No Match

Rationale: The inspected AIO targets describe language models, machine-learning tasks or training, neural architectures/layers, or a stochastic network/model class. The source-scoped symbolic SAT selector does not require those mechanisms. A possible augmented-state stochastic representation and flip-age bookkeeping do not alone establish a suitable mapping.

Search Scope: At clean merged base14e9168ee3496e914545ae5c449e3ee190f0294b, the current inventory has786 native and442 pinned AIO records:4876 identity-field occurrences,3723 normalized values, and no candidate collision. Four full-checkout searches included ignored and hidden files; all1329 distinct matching contents (23381 occurrences) were read by the attributed root/team partitions, with18 contextual fields across ten neighboring records assessed separately. This is bounded identity evidence, not proof of universal semantic absence. Exact pinned AIO CLASS neighborhoods and incident edges remain the separately accepted research assessment; 11 examined targets retain their individual rejection rationales. Shared score, memory or randomness vocabulary does not make symbolic SAT search a neural architecture or an ML training procedure.

Examined AIO Candidate	Rejection Reason
`AIO:ReasoningLLM`	The target is a language model doing reasoning in language tasks; the candidate searches Boolean assignments.
`AIO:TrainingStrategy`	A fixed-formula SAT move selector is not preprocessing or a strategy for training a machine-learning model.
`AIO:MachineLearningTask`	Keeping flip ages is bookkeeping; it does not require constructing methods that learn from data.
`AIO:ReinforcementLearning`	A probability-controlled move and clause score do not establish a learned reward policy or value-function method.
`AIO:MarkovChain`	An augmented-state stochastic description could include the assignment, ages and phase, but this representation alone does not map the named heuristic to the pinned network/model class and its probabilistic-hidden-layer relation.
`AIO:ArtificialNeuralNetwork`	The method does not require a connected network of artificial neurons.
`AIO:MemoryAugmentedLLM`	A variable-age table is not external memory in a large language model.
`AIO:MemoryCellLayer`	A SAT timestamp table is not the neural cell layer described by the target and its incident architecture edges.
`AIO:LongShortTermMemory`	The method does not require the recurrent neural architecture or its input, memory-cell and output layers.
`AIO:NoiseDenseLayer`	The discrete candidate-set coin is not dense-layer weight noise for neural regularization.
`AIO:GaussianNoiseLayer`	No additive zero-centered Gaussian regularization of neural inputs is required.

Evidence Sources & Primary Literature

2 Sources

Source ID	Publication / Document	Type / Access	Reference & Checksum
`gent-walsh1995`	Unsatisfied Variables in Local Search Ian P. Gent, Toby Walsh	primary paper full_text	sha256:eaa23fc5c52e…
`ubcsat1-hwsat`	UBCSAT 1.0.0 source archive: HWSAT selector in src/hwsat.c Dave Tompkins, UBCSAT project	official documentation documentation	sha256:62a15f14ea22…

Curation Provenance

Curator: Codex

Method: ai_assisted

Model: GPT-6

Created: 2026-10-15T23:35:54Z

Updated: 2026-10-15T23:35:54Z

Source File: data/curated/HRSAT.yaml