#!/usr/bin/env python3
"""Finite teaching checks, Python 3.10+, standard library only.

SAT oracle is exhaustive truth-table decision, deliberately not a fast solver.
Recovery receives only a boolean callable. Enumeration itself is a generator;
the harness collects tiny outputs/logs solely for comparison and reporting.
Here n is the size of the explicit dense variable table in each small fixture,
not a serialized succinct promise to output exponentially many variables.
No assertion statements: python -O retains every check.
"""
from itertools import product, combinations
from fractions import Fraction
import json


def require(condition, message):
    if not condition:
        raise RuntimeError(message)


def validate_cnf(n, clauses):
    if type(n) is not int or n < 0:
        raise ValueError("variable count must be a nonnegative integer")
    result = []
    for clause in clauses:
        row = tuple(clause)
        if any(type(k) is not int or k == 0 or abs(k) > n for k in row):
            raise ValueError("literal outside explicit variable table")
        result.append(row)
    return tuple(result)


def direct_models(n, clauses):
    """Independent reference: full assignments, no restriction operation."""
    for bits in product((0, 1), repeat=n):
        if all(any(bits[abs(k) - 1] == int(k > 0) for k in row) for row in clauses):
            yield bits


def restrict(clauses, variable, value):
    kept = []
    true_literal = variable if value else -variable
    for row in clauses:
        if true_literal in row:
            continue
        kept.append(tuple(k for k in row if k != -true_literal))
    return tuple(kept)


class BooleanSATOracle:
    def __init__(self, n, trace=False):
        self.n, self.calls, self.trace = n, 0, [] if trace else None
        self.assignment_checks = 0

    def __call__(self, clauses):
        clauses = validate_cnf(self.n, clauses)
        self.calls += 1
        # A separately written predicate evaluator, not recovery or restriction.
        answer = False
        for mask in range(1 << self.n):
            self.assignment_checks += 1
            all_true = True
            for row in clauses:
                one_true = False
                for literal in row:
                    value = bool(mask & (1 << (abs(literal) - 1)))
                    if value == (literal > 0):
                        one_true = True
                        break
                if not one_true:
                    all_true = False
                    break
            if all_true:
                answer = True
                break
        if self.trace is not None:
            self.trace.append({"clauses": clauses, "answer": answer})
        return answer


def recover_sat(n, clauses, decide):
    clauses = validate_cnf(n, clauses)
    if not decide(clauses):
        return None
    current, answer = clauses, []
    for variable in range(1, n + 1):
        trial = restrict(current, variable, 0)
        if decide(trial):
            answer.append(0)
            current = trial
        else:
            answer.append(1)
            current = restrict(current, variable, 1)
    return tuple(answer)


def enumerate_sat(n, clauses, decide):
    """Streams each model once. Depth-first stack, no previous-answer set."""
    clauses = validate_cnf(n, clauses)
    if not decide(clauses):
        return
    def visit(current, prefix):
        if len(prefix) == n:
            yield prefix
            return
        variable = len(prefix) + 1
        for value in (0, 1):
            trial = restrict(current, variable, value)
            if decide(trial):
                yield from visit(trial, prefix + (value,))
    yield from visit(clauses, ())


def recover_variable_length(bound, verify, extension):
    if not extension(""):
        return None
    prefix = ""
    while not verify(prefix):
        if len(prefix) >= bound:
            raise ValueError("inconsistent relation bound or oracle")
        prefix += "0" if extension(prefix + "0") else "1"
    return prefix


def normalize_witness(word, bound):
    if len(word) > bound or any(c not in "01" for c in word):
        raise ValueError("invalid bounded witness")
    width = bound.bit_length()  # ceil(log2(bound+1)); zero has width zero
    length = format(len(word), f"0{width}b") if width else ""
    return length + word + "0" * (bound - len(word))


def decode_witness(encoded, bound):
    width = bound.bit_length()
    if len(encoded) != width + bound or any(c not in "01" for c in encoded):
        raise ValueError("invalid fixed-length encoding")
    length = int(encoded[:width], 2) if width else 0
    if length > bound:
        raise ValueError("decoded length exceeds balance bound")
    data = encoded[width:]
    if any(c != "0" for c in data[length:]):
        raise ValueError("noncanonical padding")
    return data[:length]


def validate_knapsack(items, capacity):
    if type(capacity) is not int or capacity < 0:
        raise ValueError("capacity must be a nonnegative integer")
    if any(len(item) != 2 or any(type(a) is not int or a < 0 for a in item) for item in items):
        raise ValueError("items need nonnegative integer weight and value")


def brute_knapsack(items, capacity):
    """Independent all-subsets reference, no DP and no binary search."""
    for bits in product((0, 1), repeat=len(items)):
        weight = sum(w * b for (w, _), b in zip(items, bits))
        value = sum(v * b for (_, v), b in zip(items, bits))
        if weight <= capacity:
            yield bits, value


def capacity_dp(items, capacity):
    validate_knapsack(items, capacity)
    rows = [[0] * (capacity + 1)]
    for weight, value in items:
        previous = rows[-1]
        row = []
        for c in range(capacity + 1):
            row.append(previous[c] if weight > c else max(previous[c], previous[c - weight] + value))
        rows.append(row)
    bits, c = [0] * len(items), capacity
    for i in range(len(items), 0, -1):
        if rows[i][c] > rows[i - 1][c]:
            bits[i - 1] = 1
            c -= items[i - 1][0]
    return rows, tuple(bits)


def optimize_knapsack(items, capacity):
    validate_knapsack(items, capacity)
    calls, binary_trace, witness_trace = [], [], []
    def decide(remaining, room, target):
        result = room >= 0 and any(v >= target for _, v in brute_knapsack(remaining, room))
        calls.append({"items": remaining, "capacity": room, "threshold": target, "answer": result})
        return result
    require(decide(items, capacity, 0), "empty set should be feasible")
    low, high = 0, sum(v for _, v in items)
    while low < high:
        middle = low + (high - low + 1) // 2
        answer = decide(items, capacity, middle)
        binary_trace.append({"low": low, "high": high, "middle": middle, "answer": answer})
        if answer:
            low = middle
        else:
            high = middle - 1
    target, room, result = low, capacity, []
    for i, (weight, value) in enumerate(items):
        exclude = decide(items[i + 1:], room, target)
        chosen = 0 if exclude else 1
        witness_trace.append({"item": i + 1, "capacity": room, "target": target, "exclude_answer": exclude, "chosen": chosen})
        result.append(chosen)
        if chosen:
            room -= weight
            target -= value
    return low, tuple(result), calls, binary_trace, witness_trace


def integer_code(a):
    bits = bin(a)[2:]
    return "1" * len(bits) + "0" + bits


def sample_report():
    formula = ((1, 2), (-1, 3), (-2, -3))
    oracle = BooleanSATOracle(3, trace=True)
    witness = recover_sat(3, formula, oracle)
    enum_oracle = BooleanSATOracle(3)
    outputs, positions = [], []
    for answer in enumerate_sat(3, formula, enum_oracle):
        outputs.append(answer)
        positions.append(enum_oracle.calls)
    positions += [enum_oracle.calls]
    gaps, last = [], 0
    for count in positions:
        gaps.append(count - last)
        last = count
    items, capacity = ((4, 10), (3, 8), (2, 6)), 5
    rows, dp_witness = capacity_dp(items, capacity)
    optimum, opt_witness, calls, binary, recovery = optimize_knapsack(items, capacity)
    fields = [3, 5, 4, 10, 3, 8, 2, 6]
    lengths = [len(integer_code(a)) for a in fields]
    eps = Fraction(1, 4)
    scale = eps * 10 / 3
    scaled = [int(Fraction(v, 1) // scale) for _, v in items]
    return {"sat": {"witness": witness, "calls": oracle.calls, "queries": oracle.trace,
                    "oracle_assignment_checks": oracle.assignment_checks},
            "enumeration": {"outputs": outputs, "cumulative_calls_at_outputs_and_end": positions,
                            "call_gaps_including_end": gaps, "calls": enum_oracle.calls},
            "knapsack": {"capacity_rows": rows, "dp_witness": dp_witness, "optimum": optimum,
                         "threshold_witness": opt_witness, "calls": len(calls), "binary_trace": binary,
                         "witness_trace": recovery, "input_field_bits": lengths, "input_bits": sum(lengths),
                         "table_cells": len(rows) * len(rows[0]), "updated_cells": len(items) * len(rows[0]),
                         "scale": str(scale), "scaled_values": scaled,
                         "scaled_total_index": sum(scaled), "fptas_guarantee": str((1 - eps) * optimum)}}


def exhaustive_tests():
    sat_cases = 0
    for n in range(4):
        # Every normalized clause has absent/positive/negative choice per variable;
        # formulas include zero, one, or two such clauses, plus duplicates/tautology.
        clauses = []
        for signs in product((0, 1, -1), repeat=n):
            clauses.append(tuple((i + 1) * s for i, s in enumerate(signs) if s))
        formulae = [()] + [(c,) for c in clauses] + list(combinations(clauses, 2))
        if n:
            formulae += [((1, 1),), ((1, -1),), ((1,), (1,)), ((1,), (-1,))]
        for formula in formulae:
            expected = list(direct_models(n, formula))
            oracle = BooleanSATOracle(n)
            answer = recover_sat(n, formula, oracle)
            require(answer == (expected[0] if expected else None), "SAT lexicographic witness mismatch")
            require(oracle.calls == (n + 1 if expected else 1), "SAT query count mismatch")
            enumerator = BooleanSATOracle(n)
            actual, call_positions = [], []
            for bits in enumerate_sat(n, formula, enumerator):
                actual.append(bits)
                call_positions.append(enumerator.calls)
            require(actual == expected, "enumeration differs from independent truth table")
            last = 0
            for at in call_positions + [enumerator.calls]:
                require(at - last <= 4 * n + 2, "enumeration oracle delay exceeded")
                last = at
            sat_cases += 1
    relation_cases = 0
    universe = ["".join(s) for n in range(4) for s in product("01", repeat=n)]
    for mask in range(1 << len(universe)):
        accepted = {s for i, s in enumerate(universe) if mask >> i & 1}
        call_count = [0]
        def extension(prefix):
            call_count[0] += 1
            return any(word.startswith(prefix) for word in accepted)
        answer = recover_variable_length(3, accepted.__contains__, extension)
        require((answer in accepted) if accepted else answer is None, "variable-length search mismatch")
        require(call_count[0] <= 4, "variable-length query budget")
        relation_cases += 1
    for bound in range(6):
        for n in range(bound + 1):
            for word in map("".join, product("01", repeat=n)):
                require(decode_witness(normalize_witness(word, bound), bound) == word, "length normalization round trip")
    bad = [("1100", 2), ("0101", 2)]  # length 3>2; then padding one after length 1
    for encoded, bound in bad:
        try:
            decode_witness(encoded, bound)
        except ValueError:
            pass
        else:
            raise RuntimeError("malformed normalized witness accepted")
    knapsack_cases = 0
    catalog = tuple(product(range(3), range(3)))
    for n in range(4):
        for items in product(catalog, repeat=n):
            for capacity in range(4):
                expected = max(value for _, value in brute_knapsack(items, capacity))
                rows, bits = capacity_dp(items, capacity)
                optimum, witness, calls, _, _ = optimize_knapsack(items, capacity)
                require(rows[-1][-1] == expected == optimum, "knapsack optimum mismatch")
                for chosen in (bits, witness):
                    require(sum(w * b for (w, _), b in zip(items, chosen)) <= capacity, "overweight witness")
                    require(sum(v * b for (_, v), b in zip(items, chosen)) == expected, "wrong witness value")
                upper = sum(v for _, v in items)
                require(len(calls) <= 1 + upper.bit_length() + n, "threshold query budget")
                knapsack_cases += 1
    for n, formula in [(-1, ()), (1, ((0,),)), (1, ((2,),))]:
        try:
            recover_sat(n, formula, lambda _: True)
        except ValueError:
            pass
        else:
            raise RuntimeError("invalid CNF accepted")
    return {"cnf_cases": sat_cases, "variable_length_relations": relation_cases,
            "knapsack_cases": knapsack_cases, "malformed_encodings": "rejected",
            "scope": "finite exhaustive implementation evidence; not asymptotic or hardness proof"}


if __name__ == "__main__":
    print(json.dumps({"sample": sample_report(), "tests": exhaustive_tests()}, ensure_ascii=False, indent=2))