Sean (May 04 2020 at 21:30): Sean (May 04 2020 at 21:30):https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/
starseeker (May 05 2020 at 01:44):@Sean Is that potentially useful for boolean expression simplification?
Sean (May 05 2020 at 02:56):oh heck no :)
Sean (May 05 2020 at 03:03):in theory I'm sure one could incorporate it into some slow expression reducer, but you'd still need to encode reduction logic and null object detection. a better fit would be a compiler expression optimization pass (which are simply graph pattern match rules).
Sean (May 05 2020 at 03:06):SAT solver is needed for robust parametric constraints. "what must sph.V be to maintain dist(sph.V, arb8.F[3]) == sph.radius", i.e., keep sph tangent to arb8's 3rd face.
Last updated: Jan 09 2025 at 00:46 UTC