Page actions
instrument mechanism / verified-clean
Boolean Expression Simplifier (Karnaugh Map) mechanism
The inspectable method record for Boolean Expression Simplifier (Karnaugh Map), kept separate from implementation and qualification.
Model scope
The core Quine-McCluskey approach is mathematically appropriate for Boolean minimization, but the empty honest_label and the unspecified variable ordering, POS procedure, tie-breaking definition, and don't-care semantics prevent an unconditional PASS.
- Quine-McCluskey is a standard method for generating prime implicants and obtaining a minimal SOP, but the specification does not state that the prime-implicant chart and a covering method such as Petrick's method are used when essential implicants alone do not produce a cover.
- The claimed minimal SOP/POS output is underspecified: it must define whether minimal means fewest product/sum terms, fewest literals, or a lexicographic tie-break among equally minimal results.
- POS minimization requires an explicit procedure, such as applying Quine-McCluskey to the zero-set/maxterms or minimizing the complemented function and applying De Morgan's law; this is not stated.
- The K-map output requires a defined variable ordering and Gray-code row/column ordering; otherwise the visualization is ambiguous.
- Handling of don't-care conditions is not specified, although they materially affect Quine-McCluskey grouping and the resulting minimum expression.
Units and conventions
- Boolean values are unitless and are represented as 0=false and 1=true.
- Minterm numbering assumes the listed variables are ordered left to right with the first variable as the most-significant bit and the last variable as the least-significant bit.
- K-map rows and columns use Gray-code order; the expected grids below state their row and column labels explicitly.
- A prime mark denotes Boolean complement, + denotes OR, and juxtaposition denotes AND.
Inspectable vector
One of 4 source-bound review vectors:
{
"inputs": {
"variables": [
"A",
"B"
],
"minterms": [
1,
2,
3
],
"dont_cares": [],
"minterm_order": "A is MSB; B is LSB",
"kmap_order": {
"rows": "A=0,1",
"columns": "B=0,1"
}
},
"expected_outputs": {
"minimal_sop": "A + B",
"minimal_pos": "(A + B)",
"kmap_grid": {
"row_labels": [
"A=0",
"A=1"
],
"column_labels": [
"B=0",
"B=1"
],
"values": [
[
0,
1
],
[
1,
1
]
]
},
"spot_checks": {
"A=0,B=1": 1,
"A=1,B=0": 1,
"A=0,B=0": 0
}
},
"working": "Minterms in binary: 1=01, 2=10, 3=11. Combine 01 with 11: the A bit changes, giving -1 = B. Combine 10 with 11: the B bit changes, giving 1- = A. Minterm 1 is covered only by B, and minterm 2 is covered only by A, so both implicants are essential. Therefore SOP = A + B. The zero-set is only minterm 0 (00), so the minimal POS is the maxterm (A+B). Spot checks: A=0,B=1 gives 0+1=1; A=1,B=0 gives 1+0=1; A=0,B=0 gives 0+0=0."
}Failure boundary
BREAK_CLAIMED · SELF_FLAGGED
The specification does not state a variable bit-order convention, so minterm 1 for variables A and B can legitimately simplify to either A'B or AB'. In addition, a 32-bit signed or bitwise JavaScript implementation can mishandle minterm 4,294,967,295 by converting it to -1, even though the exact mathematical result is a 32-literal product.
Other records
Sources and evidence
These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.
VERIFIED_LEDGER.jsonevidence-tranche6/tranche6-results.jsonBOUNDARY_HAZARD_CATALOG.json