LogicMin — Boolean Logic Minimization and Verification

A small, verifiable logic optimization tool: exact two-level (SOP) minimization of single-output Boolean functions with don't-cares, built as a C++17 library plus CLI. Every result is independently re-checked against the care-set specification before it is printed, and minimality is cross-checked in the test suite against a brute-force reference that shares no code with the solver.

Scope and limits

What it does

• Exact minimization: Quine–McCluskey prime implicant generation (value+mask cube representation) followed by an exact branch-and-bound unate set cover with essential-prime extraction and column dominance.
• Explicit cost model: fewest product terms, tie-broken by fewest literals (--cost terms-literals, default), or fewest terms only (--cost terms).
• All minimum SOPs: --all enumerates every minimum-cost cover (Petrick-style), with a configurable cap.
• Honest status reporting: results are labeled optimal (search completed, cost proven minimal) or time_limit (valid cover, minimality unproven).
• Built-in verification: each emitted cover must evaluate to 1 on every ON minterm and 0 on every OFF minterm (don't-cares unconstrained), checked by an independent routine before any output is produced.
• Process tracing: --verbose prints the classic QM combining columns and prime implicant chart (to stderr, so machine-readable stdout is unchanged).

What it does not do

• 1–26 variables, single output. Exact covering is NP-hard, so very dense or highly cyclic functions may hit the time limit (then reported as such).
• It is not a heuristic multi-output minimizer: for large PLAs use Espresso; LogicMin targets small control logic (decoders, FSM next-state/output logic) where exactness and checkable results matter.
• ON and DC sets must be disjoint (some textbook examples implicitly treat overlapping entries as ON; LogicMin requires you to make that explicit).

Build and run

Requires CMake ≥ 3.16 and a C++17 compiler. No external dependencies.

cmake -S . -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build -j
ctest --test-dir build            # run the full test suite

Minimize f(a..j) = Σm(0,1,16,17,128,343,512,640,1023) + Σd(341) — the worked example from the original course assignment:

$ ./build/logicmin --vars 10 --on 0,1,16,17,128,343,512,640,1023 --dc 341
f(a,b,c,d,e,f,g,h,i,j) = b'd'e'f'g'h'i'j' + a'b'c'd'e'g'h'i' + a'bc'de'fg'hj + abcdefghij
terms = 4, literals = 35, prime implicants = 4
status: optimal (proven minimum cost)
time: 0.000028 s

Enumerate all minimum SOPs of a cyclic function (no essential primes):

$ ./build/logicmin --vars 3 --on 0,1,2,5,6,7 --all
f(a,b,c) = b'c + a'c' + ab
terms = 3, literals = 6, prime implicants = 6
status: optimal (proven minimum cost)
minimum SOPs found: 2 (complete)
  [1] b'c + a'c' + ab
  [2] bc' + a'b' + ac

Machine-readable output for scripting and benchmark harnesses:

$ ./build/logicmin --vars 4 --on 1,3,5,7 --json
{
  "tool": "logicmin",
  "version": "1.0.0",
  "num_vars": 4,
  "on": [1, 3, 5, 7],
  "dc": [],
  "status": "optimal",
  "enumeration_complete": true,
  "cost": {"terms": 1, "literals": 2},
  "verified": true,
  "primes": [
    {"pattern": "0--1", "sop": "a'd", "literals": 2}
  ],
  "solutions": [
    {"sop": "a'd", "num_terms": 1, "num_literals": 2, "terms": ["0--1"]}
  ],
  "time_seconds": 0.000011
}

--verbose prints the QM process (combining columns with v/d/x flags and the prime implicant chart) on stderr. logicmin --help lists all flags.

The library behind the CLI is a value-returning API with no I/O (logicmin::minimize, logicmin::verify in include/logicmin/logicmin.hpp), so computation, verification, and printing are fully separated — enabling the trace cannot change the computed result, and the tests assert exactly that.

Correctness evidence

All of the following run in CI (ctest) on every push, in Release and AddressSanitizer+UBSan builds on Linux plus Release on macOS:

• Care-set verification of every output. Each emitted cover is checked by an independent routine (and, in tests, additionally against the full truth table): ON minterms must evaluate to 1, OFF minterms to 0, don't-cares unconstrained.
• Exhaustive optimality for 3 variables. All 3⁸ = 6,561 possible (ON, DC) configurations are cross-checked against a brute-force reference that enumerates all 3³ cubes directly and computes the exact minimum (terms, literals) with a set-cover DP — no code shared with the QM core. On a sample of these, the --all enumeration is compared set-for-set against brute-force enumeration of all minimum covers.
• Randomized optimality for 4–5 variables (260 seeded cases) against the same brute-force reference, plus randomized functional checks up to 10 variables and 200 random small functions embedded in an 8-variable space.
• Edge cases and interface contracts: constant 0 / constant 1, duplicate inputs, invalid inputs (out-of-range, ON∩DC overlap, malformed numbers → exit code 1 with a message), multiple minimum solutions, determinism across runs, and byte-identical results with and without --verbose.

Current suite: 31 tests / ~103,000 checks.

Comparison results

Planned next (tracked in the roadmap):

• Quality/performance vs Espresso (via PyEDA's interface) on functions with don't-cares: functional equivalence on the care set, term count, literal count, runtime, and memory — exactness vs heuristic trade-off measured, not assumed.
• A hardware case study: a small opcode/address decoder written three ways (raw truth-table case, LogicMin SOP, Espresso SOP), pushed through the same Yosys/ABC flow, reporting LUT count and logic depth, with SAT equivalence checks against the specification.

Origin

This started as the NCKU Logic System Design course project (2023): a single-file Quine–McCluskey solver for 8–10 variables with a process trace (see legacy/ and the original report in docs/). It was rebuilt as a library + CLI with a value+mask core, an exact branch-and-bound cover search, verification of every output, tests, and CI.

License

MIT — see LICENSE.