Formal Computer Science / Languages & logic

Kenton Labs / Languages & logic

SAT / SMT

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

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

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.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

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.

Cost and scope

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

A common failure

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

Explore the mechanics.

Change a local input or follow the steps. The stored result and its scope remain attached to the downloadable record.

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-005
SAT / SMTA satisfiable CNF with a witnessComplete Boolean enumeration · 4 assignments

The problem

Decide (a ∨ b) ∧ (¬a ∨ b) ∧ (a ∨ ¬b). Signed literals use DIMACS-style variable numbers.

The checked result

Satisfiable: yes.

The supplied model a=true, b=true satisfies all three clauses. Enumeration checks the verdict over every assignment.

Why the checker accepts it

  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.

Formal specification

{
  "variables": 2,
  "clauses": [
    [
      1,
      2
    ],
    [
      -1,
      2
    ],
    [
      1,
      -2
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "satisfiable": true
  },
  "witness": {
    "assignment": [
      true,
      true
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 4 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

A tiny propositional instance; no solver performance claim or general SAT algorithm benchmark.

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-006 ↘Related KL-FCS-007 ↘
KL-FCS-006
SAT / SMTAn unsatisfiable CNFComplete Boolean enumeration · 2 assignments

The problem

Decide a ∧ ¬a.

The checked result

Satisfiable: no.

When a is false, the first clause fails. When a is true, the second clause fails. Enumeration covers the entire domain.

Why the checker accepts it

  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.

Formal specification

{
  "variables": 1,
  "clauses": [
    [
      1
    ],
    [
      -1
    ]
  ]
}

Claim and evidence

{
  "claim": {
    "satisfiable": false
  },
  "witness": {
    "method": "exhaustive enumeration"
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 2 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

Exhaustive enumeration is the certificate method here. This is not a DRAT/LRAT proof or a scalable UNSAT benchmark.

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-005 ↘Related KL-FCS-007 ↘
KL-FCS-007
SAT / SMTA four-bit wraparound modelComplete bit-vector enumeration · 16 values

The problem

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

The checked result

Solutions: [15].

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

Why the checker accepts it

  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.

Formal specification

{
  "width": 4,
  "addend": 1,
  "rhs": 0,
  "theory": "Unsigned four-bit values; addition modulo 16."
}

Claim and evidence

{
  "claim": {
    "solutions": [
      15
    ]
  },
  "witness": {
    "x": 15
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 16 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-005 ↘Related KL-FCS-006 ↘

Go further.

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

Questions to investigate

  1. A solver’s unverified UNSAT verdict is not a certificate. Fixed-width overflow is part of the theory.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Add checked UNSAT proof formats and solver-backed artifacts with pinned versions.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

AutomataProgramming-language semanticsType systemsFormal languagesTerm rewriting