# SAT / SMT

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.

## Acceptance procedure

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.

## Complexity

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

## Common failure

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

## Extensions

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

## Instances

- KL-FCS-005: A satisfiable CNF with a witness — Satisfiable: yes
- KL-FCS-006: An unsatisfiable CNF — Satisfiable: no
- KL-FCS-007: A four-bit wraparound model — Solutions: [15]

## References

- https://smt-lib.org/theories-FixedSizeBitVectors.shtml