mentionsVarLit
The definition implements a predicate returning true precisely when a literal matches a variable either positively or negatively. Analysts of SAT encodings in the Recognition Science complexity layer cite this when decomposing constraints into their variable supports. It is realized by exhaustive case analysis on the two constructors of the literal type.
claimFor a literal $l$ and variable index $v$ in an $n$-variable instance, the function returns true if and only if $l$ is the positive literal on $v$ or the negative literal on $v$.
background
Variables are represented as elements of Fin n. The literal type is an inductive datatype with constructors for positive and negative polarity on a variable. This definition serves as the atomic check for variable occurrence. The surrounding module defines constraints to be either disjunctive clauses or parity checks. The predicate is invoked when lifting occurrence checks from literals to clauses. Upstream results establish the literal constructors: 'Literals over n variables.' and the variable abbreviation: 'Variable indices are Fin n for a given problem size.'
proof idea
Pattern matching distinguishes the positive and negative cases of the input literal. In each branch the inner variable is compared for equality with the target using the decide tactic on the proposition u = v. The definition contains no external lemma applications.
why it matters in Recognition Science
It is the direct dependency of the clause-level occurrence predicate, which in turn supports the PC constraint machinery. Within the framework this contributes to the analysis of satisfiability problems that interface with the recognition composition law and the forcing chain steps. No open questions are directly addressed here.
scope and limits
- Does not extend to determining satisfiability of the full constraint set.
- Does not operate on XOR parity constraints.
- Does not perform variable substitution or renaming.
- Does not compute the complete support of a clause.
Lean usage
def mentionsVarClause {n} (C : Clause n) (v : Var n) : Bool := C.any (fun l => mentionsVarLit l v)formal statement (Lean)
16def mentionsVarLit {n} (l : Lit n) (v : Var n) : Bool :=
proof body
Definition body.
17 match l with
18 | .pos u => decide (u = v)
19 | .neg u => decide (u = v)
20
21/-- Whether a variable is mentioned in a clause. -/