# A four-bit wraparound model

KL-FCS-007 · SAT / SMT · version 1.0.0

## Problem

Solve x + 1 = 0 in unsigned four-bit bit-vector arithmetic.

## Context

Make satisfiability evidence explicit: a model for a positive answer, or complete finite coverage for a negative one.

## Definitions

- **CNF**: A conjunction of clauses, each a disjunction of signed literals.
- **Satisfying model**: An assignment making every clause true.
- **Bit-vector theory**: Fixed-width values with arithmetic modulo 2ʷ; distinct from unbounded integers.

## Checked result

Solutions: [15].

The value 15 wraps to 0 after adding 1. All other four-bit values fail the equality.

## Checker reasoning

1. Interpret each literal using its variable number and sign.
2. Enumerate the entire declared Boolean or bit-vector domain.
3. Check the supplied model against every constraint.
4. For unsatisfiability, require complete coverage with no satisfying assignment.

## Dataset construction

{
  "family": "sat-smt",
  "task": "Solve x + 1 = 0 in unsigned four-bit bit-vector arithmetic.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete bit-vector enumeration · 16 values",
  "acceptance": [
    "Interpret each literal using its variable number and sign.",
    "Enumerate the entire declared Boolean or bit-vector domain.",
    "Check the supplied model against every constraint.",
    "For unsatisfiability, require complete coverage with no satisfying assignment."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "width": 4,
    "addend": 1,
    "rhs": 0,
    "theory": "Unsigned four-bit values; addition modulo 16."
  },
  "claim": {
    "solutions": [
      15
    ]
  },
  "witness": {
    "x": 15
  }
}
```

## Complexity

Boolean enumeration examines 2ⁿ assignments. A width-w unary bit-vector instance examines 2ʷ values.

## Limits

A fixed bit-vector theory example checked by enumeration, not an SMT-solver run or a statement about unbounded integers.

## Common error and further work

A solver’s unverified UNSAT verdict is not a certificate. Fixed-width overflow is part of the theory.

Add checked UNSAT proof formats and solver-backed artifacts with pinned versions.

## Verification

Complete bit-vector enumeration · 16 values. 16 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://smt-lib.org/theories-FixedSizeBitVectors.shtml)