Function isPremiseSetSatisfiable

Classical satisfiability of a premise set: is there some total assignment under which every one of these premises is true?

Asked of the premise set alone — the reader's own assignment and their operator decisions play no part, which is what distinguishes it from the strong-Kleene partial evaluation the rest of the pipeline does. The two answer different questions: this one asks whether the premises can hold at all, so a false answer means the premises contradict each other and nothing may be derived through them.

Returns null for "not determined" rather than false in two cases: a group of interacting variables exceeds the ceiling, or some row could not be settled — a premise that came back neither true nor false leaves that row's answer unestablished, and false here suppresses derivation argument-wide, so it must be a claim the search actually made. A false from any one group still settles the whole set, even beside a group too large to have been walked.

The premises are split into groups sharing no variable and each group is walked over its own columns, so the cost is the sum of the groups' tables rather than their product. Every reduction here is answer-preserving: the result matches a single flat walk over all the variables at once.

ponytail: still a truth-table walk, not a SAT solver — grouping shrinks the input rather than replacing the method. Real arguments carry single-digit variable counts per group; the ceiling bounds the worst case. Reach for a solver only if null answers start showing up in practice.