GSAT clause-weighting strategy
Algorithms AIMech:GSATClauseWeighting DRAFT
A GSAT extension that starts each clause with weight one, uses weighted clause counts to select flips, and increases the weights of clauses unsatisfied by the current assignment at the end of each search attempt.
Identity Notes & Concept Scope
This is Strategy I of Selman and Kautz’s 1993 GSAT extensions. The adaptive weights guide solving the original SAT formula; they are not externally supplied weighted MAX-SAT preferences. The update occurs between attempts and uses the current end-of-attempt assignment, unlike Breakout’s reweighting at non-solution local minima within a run or Fill’s state-specific cost lifts. The paper credits Morris with an independently proposed similar approach rather than claiming exclusive invention. No normalized identity match was found across all 442 pinned AIO labels/scoped synonyms and 319 preceding native IDs/names/aliases. Full-checkout fixed-string searches included ignored and hidden files in worktree and main, returning 11 and 11 lines respectively. All eleven unique lines were inspected, and the sorted checkout hit sets were identical: source-title references and saved review/ledger frontier leads, not existing candidate records. Eight exact AIO CLASS nodes with scoped synonyms/comments and outgoing edges and six full native neighboring records were inspected. Absence is bounded to this snapshot and semantic neighborhood.
Claims & Grounded Evidence
1 Claim
Mechanism
#method
Initialize all clause weights to 1. During a GSAT attempt, count a clause according to its positive integer weight when evaluating the change in satisfied-clause score from a variable flip. Choose a best weighted-score flip with the underlying GSAT tie convention. A clause of weight L therefore contributes as if it occurred L times. At the end of an unsuccessful attempt, increment by K the weights of every clause unsatisfied by the current assignment, retain the resulting weights and begin the next attempt under the selected initialization rule. The paper normally uses K=1. Satisfaction of the original formula remains the stopping goal; adaptive weights alter move ranking but do not change which assignments satisfy all clauses. The source’s update names the current assignment, not the best assignment seen earlier in that attempt.
⚠️ Curated Limitations & Negative Results
- The source reports an empirical search extension, not a completeness or polynomial-time guarantee. Unsuccessful finite search does not certify UNSAT, and Fill’s separate completeness theorem must not be transferred to these shared clause weights.
- The update schedule matters: raising weights at every local minimum, at every flip, or according to a stored best assignment implements a different rule. The source does not prescribe a decay, cap or automatic normalization of these retained weights.
- K=1 is a reported usual choice, not a universal optimum. Positive integer weights preserve the source’s repeated-clause interpretation; arbitrary real, negative or externally fixed weights require a separate formulation.
- Attempt budgets, initialization, tie handling and the original GSAT final-flip test boundary remain implementation choices to declare. Combining the extension with other strategies does not justify inventing their interaction or reset semantics. No source solver or numerical experiment was run.
Artificial Intelligence Ontology (AIO) Grounding
Explicit AIO Snapshot Assessment: No Match
Rationale: No suitable AIO target was established for this GSAT search extension in the inspected snapshot and semantic neighborhood. Search-history reuse and adaptive penalties do not justify a forced learning-task or language-model mapping.
Search Scope: All 442 pinned AIO labels/scoped synonyms and 319 preceding native IDs/names/aliases; both full checkouts including ignored and hidden text; semantic search for SAT/search, weighting, assignment reuse, stochastic processes and evolutionary terminology; eight exact AIO CLASS nodes and six complete native neighbors.
| Examined AIO Candidate | Rejection Reason |
|---|---|
AIO:ReasoningLLM
|
Solving a supplied CNF formula does not require a language model that performs language-task reasoning. |
AIO:TrainingStrategy
|
The procedure adjusts search costs or initialization rather than requiring preprocessing to train a machine-learning model. |
AIO:MachineLearningTask
|
Retaining solver information between attempts does not by itself identify a process of developing a reusable method that learns from data. |
AIO:ReinforcementLearning
|
Adaptive clause weights or assignment reuse are not learned reward/action-value policies merely because they use search history. |
AIO:MarkovChain
|
A state representation can include search memory, but that mathematical representation alone does not ground this particular retained-weight or retained-assignment algorithm in the pinned network/model class. |
AIO:ArtificialNeuralNetwork
|
The method operates on Boolean assignments and clause scores, not a network of artificial neurons. |
AIO:EvolutionaryLLM
|
The target is a language model optimized with evolutionary computation. Its related evolutionary-algorithms synonym does not make Boolean assignment averaging a language-model architecture. |
AIO:WeightedLayer
|
Weights on SAT clauses are not values applied to cells or neurons in a network. |
Evidence Sources & Primary Literature
1 Source| Source ID | Publication / Document | Type / Access | Reference & Checksum |
|---|---|---|---|
method-source
|
Bart Selman, Henry Kautz
|
primary paper
full_text
|
sha256:f301bd7ff353…
|
Curation Provenance
Curator: Codex
Method: ai_assisted
Model: GPT-6
Created: 2026-10-11T15:33:06Z
Updated: 2026-10-11T15:33:06Z
Source File:
data/curated/GSATClauseWeighting.yaml