diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 8e0462b7a..4c91620be 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -13449,6 +13449,173 @@ These constructions use the checked sparse penalty and extraction contracts abov
   _Solution extraction._ Return the target assignment unchanged.
 ]
 
+// Reduction: ConjunctiveQueryFoldability -> Satisfiability
+#{
+  let ex = load-example("ConjunctiveQueryFoldability", "Satisfiability")
+  let src = ex.source.instance
+  let target = ex.target.instance
+  let sol = ex.solutions.at(0)
+  let d = src.domain_size
+  let x = src.num_distinguished
+  let u = src.num_undistinguished
+  let p = src.query1_conjuncts.len()
+  let q = src.query2_conjuncts.len()
+  let code(t) = if t.type == "Constant" { t.index } else if t.type == "Distinguished" {
+    d + t.index
+  } else { d + x + t.index }
+  let candidates(query) = (query.map(a => a.at(1).map(code)).flatten() +
+    if d+x+u > 0 { (0,) } else { () }).sorted().dedup()
+  let c = candidates(src.query2_conjuncts)
+  let fmt-atom(a) = $R_(#a.at(0))(#a.at(1).map(t => str(code(t))).join(", "))$
+  let image(a, w) = (a.at(0), a.at(1).map(t => if t.type == "Undistinguished" {
+    w.at(t.index)
+  } else { code(t) }))
+  let actual-image = src.query1_conjuncts.map(a => image(a, sol.source_config))
+  let target-atoms = src.query2_conjuncts.map(a => (a.at(0), a.at(1).map(code)))
+  assert(actual-image.all(a => target-atoms.contains(a)) and
+    target-atoms.all(a => actual-image.contains(a)))
+  let required(a,b) = {
+    if a.at(0) != b.at(0) { return none }
+    let req = (:)
+    for (ta,tb) in a.at(1).zip(b.at(1)) {
+      if ta.type == "Undistinguished" {
+        let key = str(ta.index)
+        let before = req.at(key, default: none)
+        if before != none and before != code(tb) { return none }
+        req.insert(key,code(tb))
+      } else if code(ta) != code(tb) { return none }
+    }
+    req.len()
+  }
+  let ksum(query) = src.query1_conjuncts.map(a => query.map(b => {
+    let k = required(a,b)
+    if k == none { 0 } else { k }
+  }).sum()).sum()
+  let k = ksum(src.query2_conjuncts)
+  let one-clauses = u*(1+c.len()*(c.len()-1)/2)
+  let one-literals = u*c.len()*c.len()
+  let match-clauses = p*q+k
+  let match-literals = p*q+3*k
+  let cover-clauses = p+q
+  let cover-literals = 2*p*q
+  let literals = target.clauses.map(a => a.literals.len()).sum()
+  assert(target.num_vars == u*c.len()+p*q)
+  assert(target.clauses.len() == one-clauses+match-clauses+cover-clauses)
+  assert(literals == one-literals+match-literals+cover-literals)
+  assert(sol.target_config.len() == target.num_vars)
+  assert(target.clauses.all(a => a.literals.any(l =>
+    sol.target_config.at(calc.abs(l)-1) == (l > 0))))
+  let selectors = sol.target_config.slice(0,u*c.len())
+  let extracted = range(u).map(y => c.at(range(c.len()).find(t => selectors.at(y*c.len()+t))))
+  assert(extracted == sol.source_config)
+  // This fixture has one distinguished term, three variables and a source loop.
+  assert(d == 0 and x == 1 and u == 3 and p == 4 and q == 3)
+  assert(src.query1_conjuncts.last().at(1).len() == 2)
+  assert(src.query1_conjuncts.last().at(1).first() == src.query1_conjuncts.last().at(1).last())
+  let v = src.query1_conjuncts.at(1).at(1).last()
+  let a = src.query2_conjuncts.at(1).at(1).first()
+  let fixed-term = src.query2_conjuncts.first().at(1).first()
+  let rel = src.query2_conjuncts.first().at(0)
+  let no-query = ((rel,(fixed-term,v)), (rel,(v,a)), (rel,(a,fixed-term)))
+  assert(no-query.all(b => b.at(1).len() == 2 and b.at(1).first() != b.at(1).last()))
+  assert(no-query.all(b => required(src.query1_conjuncts.last(),b) == none))
+  let nc = candidates(no-query).len()
+  let nk = ksum(no-query)
+  let nq = no-query.len()
+  let no-vars = u*nc+p*nq
+  let no-clauses = u*(1+nc*(nc - 1)/2)+p*nq+nk+p+nq
+  let no-literals = u*nc*nc+3*nk+3*p*nq
+  reduction-rule("ConjunctiveQueryFoldability", "Satisfiability",
+    example: true,
+    example-caption: [Exact-image query folding encoded in CNF],
+    extra: [
+      #pred-commands(
+        "pred create --example " + rule-spec(ex) + " -o cqf.json",
+        "pred path ConjunctiveQueryFoldability Satisfiability --limit all -o paths.json",
+        "pred reduce cqf.json --via route.json -o bundle.json",
+        "pred solve bundle.json",
+        "pred evaluate cqf.json --config " + cli-config(sol.source_config),
+      )
+      Select the direct entry in `paths.json` as `route.json`.
+
+      *YES example.* Encode constants first, then distinguished and
+      undistinguished variables. The fixture has $d=#d,x=#x,u=#u$,
+      $Q_1=(#src.query1_conjuncts.map(fmt-atom).join(", "))$ and
+      $Q_2=(#src.query2_conjuncts.map(fmt-atom).join(", "))$.
+      The substitution #fmt-values(sol.source_config) has exactly the required
+      image set, including a repeated image atom. Its candidates are
+      #fmt-values(c). The one-hot blocks have #one-clauses clauses and
+      #one-literals literals, the match blocks #match-clauses and
+      #match-literals, and the covers #cover-clauses and #cover-literals.
+      The target therefore has #target.num_vars variables,
+      #target.clauses.len() clauses, and #literals literal occurrences.
+      The complete witness #fmt-values(sol.target_config) satisfies every
+      clause and extracts #fmt-values(extracted).
+
+      *NO example.* Keep the fixture's source query and use
+      $Q_2=(#no-query.map(fmt-atom).join(", "))$.
+      Every target atom has unequal arguments, while the final source atom
+      repeats one variable. Its image always has equal arguments. Thus no
+      substitution has this target image. The #nq corresponding match bits
+      are forced false, contradicting their row cover, so the target is also
+      infeasible. There are #nc candidates and #nk total compatible
+      requirements, giving #no-vars variables, #no-clauses clauses and
+      #no-literals literal occurrences.
+    ],
+  )[
+    A direct one-hot CNF encoding preserves one-step exact equality of atom
+    sets. This differs from the retraction-based folding definition in
+    Chandra and Merlin @chandra1977: the present substitution need not fix
+    its image. Domain compression avoids enumerating a large constant domain.
+  ][
+    _Construction._ Let $d,x,u$ count constants, distinguished variables,
+    and undistinguished variables; put $R=d+x+u$. Number their disjoint terms
+    consecutively, and let $p,q$ be the two query-list lengths. Let $C$ be
+    the sorted terms occurring in the second query, with zero added if
+    $R>0$, and put $c=|C|$. For every variable $y$ and candidate $t$, allocate
+    selector $e_(y,t)$, imposing exactly one choice by a positive row clause
+    and all pairwise negative clauses. Allocate a match $z_(i,j)$ for each
+    source/target atom pair. Force it false if relations, fixed arguments,
+    or repeated-variable requirements conflict. Otherwise let $E_(i,j)$ be
+    its distinct required selectors and emit $(not z_(i,j) or e)$ for each
+    $e in E_(i,j)$ and $(z_(i,j) or or.big_(e in E_(i,j)) not e)$.
+    Finally require a true match in every row and every column. Empty
+    disjunctions are retained as false empty clauses.
+
+    _Correctness._ ($arrow.r.double$) In a feasible exact image, the image
+    of each variable occurring in the first query occurs in the second.
+    Unused variables can map to zero, which is legal whenever any variable
+    exists. Hence a feasible witness can use only $C$. Its selectors and
+    exact atom-equality match bits satisfy every equivalence and both covers.
+    ($arrow.l.double$) A satisfying CNF chooses a legal image for every
+    variable, and the equivalences make each match bit exactly the equality
+    of its two atoms after one substitution. Row covers give image inclusion
+    in the target; column covers give the opposite inclusion. The atom sets
+    are equal. Duplicates do not require a bijection or multiset equality.
+
+    _Solution extraction._ Validate the entire Boolean witness once, then
+    read the candidate chosen for each variable, in source-variable order.
+    Do not apply substitution recursively. Completed `Or` values map
+    identically, including infeasibility.
+
+    _Overhead._ If $K$ sums the distinct requirements over compatible pairs,
+    the exact sizes are $u c+p q$ variables,
+    $u(1+c(c-1)/2)+p q+K+p+q$ clauses and $u c^2+3K+3p q$ literals.
+    Using $c<=R$ and $K<=p q u$ gives the registered upper bounds.
+    The bounds also hold at $R=0$, where $u=c=K=0$. Nullary equal atoms
+    have a positive match unit; incompatible pairs have a negative unit.
+    With $u=0$, only fixed atom equality remains. Both empty queries are
+    feasible; exactly one empty query produces an empty cover clause.
+    Repeated variables contribute one consistent requirement each, and
+    conflicting repetitions are incompatible. The encoding is polynomial
+    in the explicit queries and witness dimension $u$, not in $log u$ alone.
+    Derived machine sizes and signed literal indices are checked; numeric
+    failure is an error, not an infeasibility answer. Metadata bounds may
+    exceed `u64` even for a tiny compressed target and then return a typed
+    range error.
+  ]
+}
+
 #let cs_sat = load-example("CircuitSAT", "Satisfiability")
 #let cs_sat_sol = cs_sat.solutions.at(0)
 #reduction-rule("CircuitSAT", "Satisfiability",
diff --git a/src/rules/conjunctivequeryfoldability_satisfiability.rs b/src/rules/conjunctivequeryfoldability_satisfiability.rs
new file mode 100644
index 000000000..9bfec56ef
--- /dev/null
+++ b/src/rules/conjunctivequeryfoldability_satisfiability.rs
@@ -0,0 +1,206 @@
+//! Reduction of exact-image conjunctive query foldability to CNF satisfiability.
+
+use crate::models::formula::{CNFClause, Satisfiability};
+use crate::models::misc::{ConjunctiveQueryFoldability, Term};
+use crate::rules::{ReduceTo, ReductionError, ReductionResult};
+use std::collections::{BTreeMap, BTreeSet};
+
+#[derive(Debug, Clone)]
+pub struct ReductionConjunctiveQueryFoldabilityToSAT {
+    target: Satisfiability,
+    candidates: Vec<usize>,
+    num_selectors: usize,
+}
+
+impl ReductionResult for ReductionConjunctiveQueryFoldabilityToSAT {
+    type Source = ConjunctiveQueryFoldability;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Satisfiability {
+        &self.target
+    }
+
+    fn extract_solution(&self, solution: &Vec<bool>) -> crate::rules::ExtractionResult<Vec<usize>> {
+        crate::rules::traits::validate_target_witness(
+            &self.target,
+            solution,
+            |value| value.0,
+            "target assignment does not satisfy the folding CNF",
+        )?;
+        Ok(solution[..self.num_selectors]
+            .iter()
+            .enumerate()
+            .filter(|(_, chosen)| **chosen)
+            .map(|(index, _)| self.candidates[index % self.candidates.len()])
+            .collect())
+    }
+}
+
+#[crate::aggregate_reduction(identity)]
+impl crate::rules::AggregateReductionResult for ReductionConjunctiveQueryFoldabilityToSAT {}
+
+fn overflow(operation: &str) -> ReductionError {
+    ReductionError::integer_overflow::<ConjunctiveQueryFoldability, Satisfiability>(operation)
+}
+
+fn variable_counts(
+    u: usize,
+    c: usize,
+    p: usize,
+    q: usize,
+) -> Result<(usize, usize), ReductionError> {
+    let selectors = u
+        .checked_mul(c)
+        .ok_or_else(|| overflow("counting selectors"))?;
+    let matches = p
+        .checked_mul(q)
+        .ok_or_else(|| overflow("counting atom matches"))?;
+    let total = selectors
+        .checked_add(matches)
+        .ok_or_else(|| overflow("counting SAT variables"))?;
+    Ok((selectors, total))
+}
+
+#[crate::reduction(transform = upper_bound {
+    num_vars = "num_undistinguished * (domain_size + num_distinguished + num_undistinguished) + num_conjuncts_q1 * num_conjuncts_q2",
+    num_clauses = "num_undistinguished * (1 + (domain_size + num_distinguished + num_undistinguished) * (domain_size + num_distinguished + num_undistinguished - 1) / 2) + num_conjuncts_q1 * num_conjuncts_q2 * (num_undistinguished + 1) + num_conjuncts_q1 + num_conjuncts_q2",
+    num_literals = "num_undistinguished * (domain_size + num_distinguished + num_undistinguished)^2 + num_conjuncts_q1 * num_conjuncts_q2 * (3 * num_undistinguished + 3)",
+})]
+impl ReduceTo<Satisfiability> for ConjunctiveQueryFoldability {
+    type Result = ReductionConjunctiveQueryFoldabilityToSAT;
+
+    fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
+        let d = self.domain_size();
+        let u = self.num_undistinguished();
+        let fixed = d
+            .checked_add(self.num_distinguished())
+            .ok_or_else(|| overflow("counting fixed terms"))?;
+        let range = fixed
+            .checked_add(u)
+            .ok_or_else(|| overflow("counting all terms"))?;
+        let index = |term: &Term| match *term {
+            Term::Constant(i) => i,
+            Term::Distinguished(i) => d + i,
+            Term::Undistinguished(i) => fixed + i,
+        };
+        let mut terms = BTreeSet::new();
+        if range > 0 {
+            terms.insert(0);
+        }
+        for (_, args) in self.query2_conjuncts() {
+            terms.extend(args.iter().map(index));
+        }
+        let candidates: Vec<_> = terms.into_iter().collect();
+        let c = candidates.len();
+        let p = self.num_conjuncts_q1();
+        let q = self.num_conjuncts_q2();
+        let (num_selectors, num_vars) = variable_counts(u, c, p, q)?;
+        Self::exact_i64(num_vars, "representing SAT literal indices")?;
+        // Every offset below is bounded by the checked total variable count.
+        let selector = |y, t| Self::exact_i64(y * c + t + 1, "numbering selectors");
+        let match_bit = |i, j| Self::exact_i64(num_selectors + i * q + j + 1, "numbering matches");
+        let mut clauses = Vec::new();
+        for y in 0..u {
+            clauses.push(CNFClause::new(
+                (0..c).map(|t| selector(y, t)).collect::<Result<_, _>>()?,
+            ));
+            for t in 0..c {
+                for s in t + 1..c {
+                    clauses.push(CNFClause::new(vec![-selector(y, t)?, -selector(y, s)?]));
+                }
+            }
+        }
+        for (i, (ra, aa)) in self.query1_conjuncts().iter().enumerate() {
+            for (j, (rb, ab)) in self.query2_conjuncts().iter().enumerate() {
+                let z = match_bit(i, j)?;
+                let mut compatible = ra == rb;
+                let mut requirements = BTreeMap::new();
+                if compatible {
+                    for (a, b) in aa.iter().zip(ab) {
+                        let b = index(b);
+                        match a {
+                            Term::Undistinguished(y) => {
+                                if let Some(previous) = requirements.insert(*y, b) {
+                                    compatible &= previous == b;
+                                }
+                            }
+                            _ => compatible &= index(a) == b,
+                        }
+                    }
+                }
+                if !compatible {
+                    clauses.push(CNFClause::new(vec![-z]));
+                    continue;
+                }
+                let mut reverse = vec![z];
+                for (y, term) in requirements {
+                    let t = candidates
+                        .binary_search(&term)
+                        .expect("target terms are candidates");
+                    let e = selector(y, t)?;
+                    clauses.push(CNFClause::new(vec![-z, e]));
+                    reverse.push(-e);
+                }
+                clauses.push(CNFClause::new(reverse));
+            }
+        }
+        for i in 0..p {
+            clauses.push(CNFClause::new(
+                (0..q).map(|j| match_bit(i, j)).collect::<Result<_, _>>()?,
+            ));
+        }
+        for j in 0..q {
+            clauses.push(CNFClause::new(
+                (0..p).map(|i| match_bit(i, j)).collect::<Result<_, _>>()?,
+            ));
+        }
+        let target =
+            Satisfiability::try_new(num_vars, clauses).map_err(Self::target_construction)?;
+        Ok(ReductionConjunctiveQueryFoldabilityToSAT {
+            target,
+            candidates,
+            num_selectors,
+        })
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+    use Term::{Distinguished as X, Undistinguished as Y};
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "conjunctivequeryfoldability_to_satisfiability",
+        build: || {
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                ConjunctiveQueryFoldability::new(
+                    0,
+                    1,
+                    3,
+                    vec![2],
+                    vec![
+                        (0, vec![X(0), Y(0)]),
+                        (0, vec![Y(0), Y(1)]),
+                        (0, vec![Y(1), X(0)]),
+                        (0, vec![Y(0), Y(0)]),
+                    ],
+                    vec![
+                        (0, vec![X(0), Y(2)]),
+                        (0, vec![Y(2), Y(2)]),
+                        (0, vec![Y(2), X(0)]),
+                    ],
+                ),
+                SolutionPair {
+                    source_config: serde_json::json!([3, 3, 3]),
+                    target_config: serde_json::json!([
+                        false, true, false, true, false, true, true, false, false, false, true,
+                        false, false, false, true, false, true, false
+                    ]),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/conjunctivequeryfoldability_satisfiability.rs"]
+mod tests;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 7606f4923..b5ace8d9a 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -24,6 +24,7 @@ pub(crate) mod circuit_sat;
 pub(crate) mod circuit_spinglass;
 mod closestvectorproblem_qubo;
 pub(crate) mod coloring_qubo;
+pub(crate) mod conjunctivequeryfoldability_satisfiability;
 pub(crate) mod cyclicordering_ilp;
 pub(crate) mod decisionmaximumindependentset_integralflowbundles;
 pub(crate) mod decisionminimumdominatingset_minimumsummulticenter;
@@ -355,6 +356,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(staffscheduling_qubo::canonical_rule_example_specs());
     specs.extend(closestvectorproblem_qubo::canonical_rule_example_specs());
     specs.extend(coloring_qubo::canonical_rule_example_specs());
+    specs.extend(conjunctivequeryfoldability_satisfiability::canonical_rule_example_specs());
     specs.extend(sequencingtominimizeweightedcompletiontime_qubo::canonical_rule_example_specs());
     specs.extend(schedulingwithindividualdeadlines_qubo::canonical_rule_example_specs());
     specs.extend(precedenceconstrainedscheduling_qubo::canonical_rule_example_specs());
diff --git a/src/unit_tests/rules/conjunctivequeryfoldability_satisfiability.rs b/src/unit_tests/rules/conjunctivequeryfoldability_satisfiability.rs
new file mode 100644
index 000000000..c7c8801fa
--- /dev/null
+++ b/src/unit_tests/rules/conjunctivequeryfoldability_satisfiability.rs
@@ -0,0 +1,506 @@
+use super::*;
+use crate::models::misc::Term;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
+use crate::{BruteForce, Problem};
+
+fn example(no: bool) -> ConjunctiveQueryFoldability {
+    use Term::{Distinguished as X, Undistinguished as Y};
+    ConjunctiveQueryFoldability::new(
+        0,
+        1,
+        3,
+        vec![2],
+        vec![
+            (0, vec![X(0), Y(0)]),
+            (0, vec![Y(0), Y(1)]),
+            (0, vec![Y(1), X(0)]),
+            (0, vec![Y(0), Y(0)]),
+        ],
+        if no {
+            vec![
+                (0, vec![X(0), Y(1)]),
+                (0, vec![Y(1), Y(2)]),
+                (0, vec![Y(2), X(0)]),
+            ]
+        } else {
+            vec![
+                (0, vec![X(0), Y(2)]),
+                (0, vec![Y(2), Y(2)]),
+                (0, vec![Y(2), X(0)]),
+            ]
+        },
+    )
+}
+
+fn reduce(source: &ConjunctiveQueryFoldability) -> ReductionConjunctiveQueryFoldabilityToSAT {
+    ReduceTo::<Satisfiability>::reduce_to(source).unwrap()
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_closed_loop() {
+    use Term::Undistinguished as Y;
+    let source = ConjunctiveQueryFoldability::new(
+        0,
+        0,
+        2,
+        vec![2],
+        vec![(0, vec![Y(0), Y(1)])],
+        vec![(0, vec![Y(1), Y(0)])],
+    );
+    let reduction = reduce(&source);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduction,
+        "query fold to SAT",
+    );
+    let witness = BruteForce::new()
+        .solve(reduction.target_problem())
+        .unwrap()
+        .unwrap();
+    assert_eq!(reduction.extract_solution(&witness).unwrap(), vec![1, 0]);
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_worked_examples() {
+    let yes = example(false);
+    let reduction = reduce(&yes);
+    let t = reduction.target_problem();
+    assert_eq!(
+        (t.num_vars(), t.num_clauses(), t.num_literals()),
+        (18, 34, 75)
+    );
+    let witness = [
+        false, true, false, true, false, true, true, false, false, false, true, false, false,
+        false, true, false, true, false,
+    ]
+    .to_vec();
+    assert!(t.evaluate(&witness).unwrap().0);
+    assert_eq!(reduction.extract_solution(&witness).unwrap(), vec![3, 3, 3]);
+    assert!(yes.evaluate(&vec![3, 3, 3]).unwrap().0);
+    let no = example(true);
+    let r = reduce(&no);
+    let t = r.target_problem();
+    assert_eq!(
+        (t.num_vars(), t.num_clauses(), t.num_literals()),
+        (21, 39, 87)
+    );
+    assert!(BruteForce::new().solve(&no).unwrap().is_none());
+    for z in 19..=21 {
+        assert!(t.clauses().iter().any(|clause| clause.literals == vec![-z]));
+    }
+    assert!(
+        t.clauses()
+            .iter()
+            .any(|clause| clause.literals == vec![19, 20, 21])
+    );
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_rejects_invalid_witnesses() {
+    let reduction = reduce(&example(false));
+    assert!(reduction.extract_solution(&vec![false; 17]).is_err());
+    assert!(reduction.extract_solution(&vec![false; 19]).is_err());
+    assert!(reduction.extract_solution(&vec![false; 18]).is_err());
+    assert!(reduction.extract_solution(&vec![true; 18]).is_err());
+}
+
+#[cfg(feature = "example-db")]
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_canonical_export() {
+    let spec = canonical_rule_example_specs().remove(0);
+    let exported = (spec.build)();
+    let source: ConjunctiveQueryFoldability =
+        serde_json::from_value(exported.source.instance).unwrap();
+    let target: Satisfiability = serde_json::from_value(exported.target.instance).unwrap();
+    let pair = &exported.solutions[0];
+    let w: Vec<usize> = serde_json::from_value(pair.source_config.clone()).unwrap();
+    let b: Vec<bool> = serde_json::from_value(pair.target_config.clone()).unwrap();
+    assert_eq!(
+        serde_json::to_value(&source).unwrap(),
+        serde_json::to_value(example(false)).unwrap()
+    );
+    assert_eq!(
+        (
+            target.num_vars(),
+            target.num_clauses(),
+            target.num_literals()
+        ),
+        (18, 34, 75)
+    );
+    assert!(source.evaluate(&w).unwrap().0);
+    assert!(target.evaluate(&b).unwrap().0);
+    assert_eq!(reduce(&source).extract_solution(&b).unwrap(), w);
+}
+
+// Generic CNF enumeration with unit propagation; tiny cases are checked against BruteForce.
+fn sat_models(target: &Satisfiability) -> Vec<Vec<bool>> {
+    fn visit(target: &Satisfiability, mut values: Vec<Option<bool>>, out: &mut Vec<Vec<bool>>) {
+        loop {
+            let mut forced = None;
+            for clause in target.clauses() {
+                let mut unknown = Vec::new();
+                let mut satisfied = false;
+                for &lit in &clause.literals {
+                    let v = usize::try_from(lit.unsigned_abs()).unwrap() - 1;
+                    match values[v] {
+                        Some(value) => satisfied |= value == (lit > 0),
+                        None => unknown.push((v, lit > 0)),
+                    }
+                }
+                if satisfied {
+                    continue;
+                }
+                if unknown.is_empty() {
+                    return;
+                }
+                if unknown.len() == 1 {
+                    forced = Some(unknown[0]);
+                    break;
+                }
+            }
+            if let Some((v, value)) = forced {
+                values[v] = Some(value);
+            } else {
+                break;
+            }
+        }
+        if let Some(v) = values.iter().position(Option::is_none) {
+            for value in [false, true] {
+                let mut next = values.clone();
+                next[v] = Some(value);
+                visit(target, next, out);
+            }
+        } else {
+            let bits: Vec<_> = values.into_iter().map(Option::unwrap).collect();
+            assert!(target.evaluate(&bits).unwrap().0);
+            out.push(bits);
+        }
+    }
+    let mut out = Vec::new();
+    visit(target, vec![None; target.num_vars()], &mut out);
+    out.sort();
+    out
+}
+
+fn source_feasible(source: &ConjunctiveQueryFoldability) -> bool {
+    fn search(
+        s: &ConjunctiveQueryFoldability,
+        used: &[usize],
+        w: &mut Vec<usize>,
+        range: usize,
+    ) -> bool {
+        let Some((&y, rest)) = used.split_first() else {
+            return s.evaluate(w).unwrap().0;
+        };
+        (0..range).any(|value| {
+            w[y] = value;
+            search(s, rest, w, range)
+        })
+    }
+    // Unused coordinates cannot change an atom image; still enumerate the full term domain.
+    let used: std::collections::BTreeSet<_> = source
+        .query1_conjuncts()
+        .iter()
+        .flat_map(|(_, args)| args)
+        .filter_map(|t| match t {
+            Term::Undistinguished(y) => Some(*y),
+            _ => None,
+        })
+        .collect();
+    search(
+        source,
+        &used.into_iter().collect::<Vec<_>>(),
+        &mut vec![0; source.num_undistinguished()],
+        source.domain_size() + source.num_distinguished() + source.num_undistinguished(),
+    )
+}
+
+fn audit(source: &ConjunctiveQueryFoldability, raw: bool) {
+    let r = reduce(source);
+    let target = r.target_problem();
+    let models = sat_models(target);
+    let direct = source_feasible(source);
+    assert_eq!(direct, !models.is_empty(), "{source:?}");
+    assert_eq!(
+        crate::rules::AggregateReductionResult::extract_value(
+            &r,
+            crate::types::Or(!models.is_empty())
+        )
+        .0,
+        direct
+    );
+    for bits in &models {
+        let w = r.extract_solution(bits).unwrap();
+        assert!(source.evaluate(&w).unwrap().0);
+        for y in 0..source.num_undistinguished() {
+            assert_eq!(
+                bits[y * r.candidates.len()..(y + 1) * r.candidates.len()]
+                    .iter()
+                    .filter(|&&b| b)
+                    .count(),
+                1
+            );
+        }
+    }
+    if raw {
+        assert_eq!(direct, BruteForce::new().solve(source).unwrap().is_some());
+    }
+    if raw && target.num_vars() <= 10 {
+        let mut reference = BruteForce::new().find_all_witnesses(target).unwrap();
+        reference.sort();
+        assert_eq!(models, reference);
+        for mask in 0..(1usize << target.num_vars()) {
+            let bits: Vec<_> = (0..target.num_vars())
+                .map(|i| mask & (1 << i) != 0)
+                .collect();
+            assert_eq!(
+                r.extract_solution(&bits).is_ok(),
+                target.evaluate(&bits).unwrap().0
+            );
+        }
+    }
+    crate::rules::test_helpers::assert_parameter_predictions(source, &r);
+}
+
+fn from_codes(
+    d: usize,
+    x: usize,
+    u: usize,
+    arities: Vec<usize>,
+    a: Vec<(usize, Vec<usize>)>,
+    b: Vec<(usize, Vec<usize>)>,
+) -> ConjunctiveQueryFoldability {
+    let term = |v| {
+        if v < d {
+            Term::Constant(v)
+        } else if v < d + x {
+            Term::Distinguished(v - d)
+        } else {
+            Term::Undistinguished(v - d - x)
+        }
+    };
+    let query = |atoms: Vec<(usize, Vec<usize>)>| {
+        atoms
+            .into_iter()
+            .map(|(rel, args)| (rel, args.into_iter().map(term).collect()))
+            .collect()
+    };
+    ConjunctiveQueryFoldability::new(d, x, u, arities, query(a), query(b))
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_exhaustive_unary_lists() {
+    let mut lists = vec![vec![]];
+    for a in 0..2 {
+        lists.push(vec![(0, vec![a])]);
+        for b in 0..2 {
+            lists.push(vec![(0, vec![a]), (0, vec![b])]);
+        }
+    }
+    for (d, x, u) in [(0, 0, 2), (0, 1, 1), (1, 0, 1), (1, 1, 0)] {
+        for a in &lists {
+            for b in &lists {
+                audit(&from_codes(d, x, u, vec![1], a.clone(), b.clone()), true);
+            }
+        }
+    }
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_empty_universe_and_nullary_sets() {
+    let mut lists = vec![vec![]];
+    for a in 0..2 {
+        lists.push(vec![(a, vec![])]);
+        for b in 0..2 {
+            lists.push(vec![(a, vec![]), (b, vec![])]);
+        }
+    }
+    for a in &lists {
+        for b in &lists {
+            audit(&from_codes(0, 0, 0, vec![0, 0], a.clone(), b.clone()), true);
+        }
+    }
+    for u in [0, 3] {
+        audit(&from_codes(0, 0, u, vec![], vec![], vec![]), true);
+    }
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_repeated_full_arity_arguments() {
+    for u in 1..=5 {
+        let args: Vec<_> = (0..u).collect();
+        let images: Vec<_> = (0..u).rev().collect();
+        for copies in [1, 2] {
+            audit(
+                &from_codes(
+                    0,
+                    0,
+                    u,
+                    vec![u * copies],
+                    vec![(0, args.repeat(copies))],
+                    vec![(0, images.repeat(copies))],
+                ),
+                true,
+            );
+        }
+        if u > 1 {
+            let mut conflict = images.repeat(2);
+            conflict[2 * u - 1] = 1;
+            let source = from_codes(
+                0,
+                0,
+                u,
+                vec![2 * u],
+                vec![(0, args.repeat(2))],
+                vec![(0, conflict)],
+            );
+            assert!(BruteForce::new().solve(&source).unwrap().is_none());
+            audit(&source, true);
+        }
+    }
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_large_compressed_domains() {
+    for d in [1usize << 32, usize::MAX - 2] {
+        let s = from_codes(d, 1, 1, vec![1], vec![(0, vec![d + 1])], vec![(0, vec![d])]);
+        let r = reduce(&s);
+        assert_eq!(r.candidates, vec![0, d]);
+        assert_eq!(
+            (
+                r.target.num_vars(),
+                r.target.num_clauses(),
+                r.target.num_literals()
+            ),
+            (3, 6, 10)
+        );
+        for b in sat_models(&r.target) {
+            assert_eq!(r.extract_solution(&b).unwrap(), vec![d]);
+            assert!(s.evaluate(&vec![d]).unwrap().0);
+        }
+        let entry = crate::rules::registry::reduction_entries()
+            .into_iter()
+            .find(|e| {
+                e.source_name == ConjunctiveQueryFoldability::NAME
+                    && e.target_name == Satisfiability::NAME
+            })
+            .unwrap();
+        assert!(matches!(
+            entry
+                .parameter_contract()
+                .unwrap()
+                .transform()
+                .unwrap()
+                .evaluate(&s.parameters()),
+            Err(crate::parameters::ParameterTransformError::OutputOutOfRange { .. })
+        ));
+    }
+}
+
+#[test]
+fn test_conjunctivequeryfoldability_to_satisfiability_numeric_boundaries() {
+    // These arithmetic boundaries cannot be exercised by allocating their target vectors.
+    assert_eq!(
+        variable_counts(usize::MAX, 1, 0, 0).unwrap(),
+        (usize::MAX, usize::MAX)
+    );
+    assert!(matches!(
+        variable_counts(usize::MAX, 2, 0, 0),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    assert_eq!(
+        variable_counts(0, 0, usize::MAX, 1).unwrap(),
+        (0, usize::MAX)
+    );
+    assert!(matches!(
+        variable_counts(0, 0, usize::MAX, 2),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    assert_eq!(
+        variable_counts(usize::MAX - 1, 1, 1, 1).unwrap(),
+        (usize::MAX - 1, usize::MAX)
+    );
+    assert!(matches!(
+        variable_counts(usize::MAX, 1, 1, 1),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    let limit = usize::try_from(i64::MAX).unwrap();
+    assert_eq!(
+        <ConjunctiveQueryFoldability as ReduceTo<Satisfiability>>::exact_i64(
+            limit,
+            "literal index"
+        )
+        .unwrap(),
+        i64::MAX
+    );
+    let oversized = ConjunctiveQueryFoldability::new(0, 0, limit + 1, vec![], vec![], vec![]);
+    assert!(matches!(
+        ReduceTo::<Satisfiability>::reduce_to(&oversized),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    let fixed_boundary =
+        ConjunctiveQueryFoldability::new(usize::MAX - 1, 1, 0, vec![], vec![], vec![]);
+    assert_eq!(reduce(&fixed_boundary).target.num_vars(), 0);
+    for (d, x, u) in [(usize::MAX, 1, 0), (usize::MAX - 1, 1, 1)] {
+        let s = ConjunctiveQueryFoldability::new(d, x, u, vec![], vec![], vec![]);
+        assert!(matches!(
+            ReduceTo::<Satisfiability>::reduce_to(&s),
+            Err(ReductionError::IntegerOverflow { .. })
+        ));
+    }
+}
+
+fn sampled_cell(u: usize, m: usize) {
+    use rand::{RngExt, SeedableRng};
+    let mut rng = rand::rngs::StdRng::seed_from_u64(2026101305 + u64::try_from(u * 6 + m).unwrap());
+    for _ in 0..300 {
+        let d = rng.random_range(0..=1);
+        let x = rng.random_range(0..=1);
+        let range = d + x + u;
+        let arities = if range == 0 {
+            vec![0, 0]
+        } else {
+            vec![0, 0, 1, 2]
+        };
+        let atoms: Vec<_> = (0..m)
+            .map(|_| {
+                let rel = rng.random_range(0..arities.len());
+                (
+                    rel,
+                    (0..arities[rel])
+                        .map(|_| rng.random_range(0..range))
+                        .collect(),
+                )
+            })
+            .collect();
+        let p = rng.random_range(0..=m);
+        let source = from_codes(d, x, u, arities, atoms[..p].to_vec(), atoms[p..].to_vec());
+        audit(&source, false);
+    }
+}
+
+macro_rules! sampled_cells {
+    ($u:expr; $($name:ident => $m:expr),+ $(,)?) => { $(
+        #[test]
+        fn $name() { sampled_cell($u,$m); }
+    )+ };
+}
+
+sampled_cells!(0; sample_fixed_empty => 0, sample_fixed_one_atom => 1,
+    sample_fixed_two_atoms => 2, sample_fixed_three_atoms => 3,
+    sample_fixed_four_atoms => 4, sample_fixed_five_atoms => 5);
+sampled_cells!(1; sample_one_variable_empty => 0, sample_one_variable_one_atom => 1,
+    sample_one_variable_two_atoms => 2, sample_one_variable_three_atoms => 3,
+    sample_one_variable_four_atoms => 4, sample_one_variable_five_atoms => 5);
+sampled_cells!(2; sample_two_variables_empty => 0, sample_two_variables_one_atom => 1,
+    sample_two_variables_two_atoms => 2, sample_two_variables_three_atoms => 3,
+    sample_two_variables_four_atoms => 4, sample_two_variables_five_atoms => 5);
+sampled_cells!(3; sample_three_variables_empty => 0, sample_three_variables_one_atom => 1,
+    sample_three_variables_two_atoms => 2, sample_three_variables_three_atoms => 3,
+    sample_three_variables_four_atoms => 4, sample_three_variables_five_atoms => 5);
+sampled_cells!(4; sample_four_variables_empty => 0, sample_four_variables_one_atom => 1,
+    sample_four_variables_two_atoms => 2, sample_four_variables_three_atoms => 3,
+    sample_four_variables_four_atoms => 4, sample_four_variables_five_atoms => 5);
+sampled_cells!(5; sample_five_variables_empty => 0, sample_five_variables_one_atom => 1,
+    sample_five_variables_two_atoms => 2, sample_five_variables_three_atoms => 3,
+    sample_five_variables_four_atoms => 4, sample_five_variables_five_atoms => 5);