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;
/**
 * The answer of `findSatisfyingAssignment`: satisfiable with one witness,
 * unsatisfiable, or not determined.
 */
export type TSatisfyingAssignmentResult = {
    satisfiable: true;
    assignment: Record<string, boolean>;
} | {
    satisfiable: false;
} | {
    satisfiable: null;
};
/**
 * The same search as `isPremiseSetSatisfiable`, answering with one satisfying
 * assignment when there is one.
 *
 * The witness merges the first satisfying row of each group of interacting
 * variables. It holds a value for every variable the walk varied — every free
 * variable some premise reaches — and `true` for every forced-true variable. A
 * free variable no premise reaches is absent: no premise reads it, so any
 * value satisfies.
 *
 * The answer is `{ satisfiable: null }` exactly where `isPremiseSetSatisfiable`
 * returns `null`, including when a group exceeds
 * `SATISFIABILITY_VARIABLE_CEILING` — no witness is offered for a set the
 * search could not finish.
 */
export declare function findSatisfyingAssignment(ctx: TArgumentEvaluationContext, input: TPremiseSetSatisfiabilityInput): TSatisfyingAssignmentResult;
//# sourceMappingURL=satisfiability.d.ts.map