AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug ~~Donate~~ Contacts

← Back to list of members

SolveTable(AngouriMath.Entity,AngouriMath.Entity.Variable[])

Method (no overloads)

Summary

Returns a tensor of solutions over variables so that
the expression turns into a True when evaled.

Remarks

Assigns the variables one at a time and asks after each what the expression
already is. A prefix that makes it false rules out every completion of itself at
once, and a prefix that makes it true admits all of them, so neither has to be
walked. Only a prefix that settles nothing is branched on. Enumerating all
2^n rows and testing each — which is what this did — is the case where no
prefix ever settles anything, and is now the worst case rather than the only one.
The order of the rows is unchanged: assigning false before true, with the last
variable moving fastest, is the same order counting through the table produced.
This enumerates models, not satisfiability, so the result can still be
exponentially large — a tautology over n variables has 2^n solutions and they all
have to be written down. What is gone is paying that price for the search when the
answer is small.

AngouriMath

Table of contents

AngouriMath

SolveTable​(AngouriMath.​Entity,​AngouriMath.​Entity.​Variable[])

SolveTable(AngouriMath.Entity,AngouriMath.Entity.Variable[])