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.
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
truefor 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 whereisPremiseSetSatisfiablereturnsnull, including when a group exceedsSATISFIABILITY_VARIABLE_CEILING— no witness is offered for a set the search could not finish.