Papadimitriou 2-SAT random walk
Algorithms AIMech:Papadimitriou2SATRandomWalk DRAFT
A randomized 2-SAT search procedure that starts from any complete truth assignment and repeatedly selects an unsatisfied clause and flips a uniformly chosen literal’s variable until a satisfying assignment is reached or a selected move budget ends.
Identity Notes & Concept Scope
The record captures the 2-SAT application and Theorem 5 of Papadimitriou’s 1991 paper. It is distinct from that paper’s more general preference-graph and undominated-model problems, from greedy/random mixtures in GWSAT, from WalkSAT/SKC’s zero-break priority, and from later bounded-walk/restart algorithms for general k-SAT. The original short rule permits any starting assignment and does not demand a uniformly random clause-selection rule. 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
For a CNF formula whose clauses contain at most two literals, keep a complete assignment. If it satisfies every clause, return that assignment. Otherwise choose an unsatisfied nonempty clause, sample one of its literals uniformly, flip the corresponding variable and repeat. The selected clause becomes satisfied, although other clauses can become unsatisfied. Theorem 5 states that on a satisfiable 2-SAT formula, enough O(n²) such moves find a model with probability arbitrarily close to one, where n is the number of variables. Its proof sketch fixes a satisfying witness and compares Hamming distance to a reflecting gambler’s-ruin walk: a step is at least as likely to reduce that distance as increase it, and distance is bounded above by n. The hidden time factor depends on the chosen confidence; the record interprets O(n²) as a move-count statement for fixed desired error, not one constant for arbitrarily small failure probabilities.
⚠️ Curated Limitations & Negative Results
- A verified satisfying assignment is a sound positive result. Failure within a finite budget can occur on a satisfiable formula and is not a proof of unsatisfiability; the theorem describes a one-sided randomized search/decision guarantee.
- The 2-SAT analysis does not establish the same bound for general CNF, greedy mixtures, SKC priorities or arbitrary biased literal selection. A chosen clause-selection policy and formula representation must be explicit; the literal choice is random even when clause choice is deterministic.
- The source’s bound counts moves and does not make locating an unsatisfied clause or updating formula data structures free in wall-clock complexity. The short proof is a sketch, not a fully specified executable implementation or a numerical benchmark.
- Empty clauses provide no literal to flip and need separate handling. An empty conjunction is already satisfied. The inspected method does not prescribe a restart schedule, mandatory random initialization or a universal fixed cutoff constant.
- The primary paper motivates related random walks through Markov chains. With a clause-selection policy depending only on the current assignment, the transition rule is a Markov chain; arbitrary history-dependent choices need not have that property on the assignment state alone. This does not identify the algorithm with a neural network.
Artificial Intelligence Ontology (AIO) Grounding
Mapped AIO Classes
| AIO Target Class | Mapping Relation | Mapping Rationale |
|---|---|---|
AIO:MarkovChain
Markov Chain
|
related_match | The primary paper explicitly develops a Markov-chain interpretation and uses a reflecting random-walk comparison for the 2-SAT theorem. This is an algorithm-to-stochastic-process association, not equivalence or an is-a mapping to the pinned Network hierarchy. A clause-selection policy based only on the current assignment gives a state-based chain; history-dependent choices require additional state and are not silently assumed memoryless. |
Evidence Sources & Primary Literature
1 Source| Source ID | Publication / Document | Type / Access | Reference & Checksum |
|---|---|---|---|
method-source
|
Christos H. Papadimitriou
|
primary paper
full_text
|
sha256:c7d6013bff13…
|
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/Papadimitriou2SATRandomWalk.yaml