Satisfiable
Satisfiability for a CNF formula over n variables is defined as the existence of a Boolean assignment that makes the full conjunction evaluate to true. Researchers working on SAT-to-J-cost encodings or BWD-3 linear feasibility reductions cite this predicate to connect classical satisfiability with Recognition Science cost functions. The definition is a direct existential statement over the Assignment type using the evalCNF aggregator.
claimA CNF formula $φ$ with $n$ variables is satisfiable when there exists an assignment $a$ from the $n$ variables to Boolean values such that the conjunction of all clause evaluations under $a$ equals true.
background
CNF is a structure holding a list of clauses over variables indexed by Fin n, with the empty list evaluating to true. Assignment is the type of total functions from these variables to Bool, and evalCNF computes the logical AND across clause results. The module sets variable indices explicitly as Fin n for finite problem size.
proof idea
One-line definition that directly introduces the Prop via existential quantification over Assignment n and the predicate evalCNF a φ = true. It depends on the upstream evalCNF aggregator and the two Assignment aliases.
why it matters in Recognition Science
This predicate is the central interface for the SAT module. It appears in the sound field of BWD3Model, in satJCost_zero_iff from RSatEncoding, and in the classical decider theorems sat_decider_classical and satisfiable_iff_linearFeasible. It supplies the logical bridge from CNF satisfiability to linear feasibility and J-cost zero conditions inside the Recognition framework.
scope and limits
- Does not encode any search procedure for the witnessing assignment.
- Does not restrict clause length or literal polarity.
- Does not address uniqueness of solutions.
- Does not extend beyond finite n.
formal statement (Lean)
41def Satisfiable {n} (φ : CNF n) : Prop :=
proof body
Definition body.
42 ∃ a : Assignment n, evalCNF a φ = true
43
44/-- Uniquely satisfiable CNF. -/
used by (12)
-
satJCost_zero_iff -
BWD3Model -
sat_decider_classical -
sat_decider_from_rank_test -
satisfiable_iff_linearFeasible -
evalCNF -
geometric_isolation_enables_propagation_hypothesis -
geometric_isolation_enables_propagation_thm -
polynomial_time_3sat_algorithm -
polynomial_time_3sat_algorithm_hypothesis -
IsolatingFamily -
CNFWithXOR