import type { TCoreTrivalentValue } from "../../types/evaluation.js";
import type { TArgumentEvaluationContext, TEvaluablePremise } from "./argument-evaluation.js";
/**
 * Free-variable ceiling for the satisfiability walk, applied to each group of
 * interacting variables rather than to their total. Beyond it that group's
 * answer is reported as "not determined" rather than paid for.
 */
export declare const SATISFIABILITY_VARIABLE_CEILING = 16;
export interface TPremiseSetSatisfiabilityInput {
    /** The premises that must come out true together. */
    premises: TEvaluablePremise[];
    /**
     * Variable IDs available to enumerate over — the same claim-bound and
     * externally-bound set evaluation uses. Internally premise-bound
     * variables resolve lazily and get no column. Passing more than the
     * premises reach is harmless: an id no premise can reach gets no column.
     */
    freeVariableIds: string[];
    /** Variable IDs pinned `true` in every row, and given no column. */
    forcedTrueVariableIds?: ReadonlySet<string>;
}
/**
 * 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.
 */
export declare function isPremiseSetSatisfiable(ctx: TArgumentEvaluationContext, input: TPremiseSetSatisfiabilityInput): TCoreTrivalentValue;
//# sourceMappingURL=satisfiability.d.ts.map