Stream: brlcad

Topic: SAT solver


view this post on Zulip Sean (May 04 2020 at 21:30):

https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/

view this post on Zulip starseeker (May 05 2020 at 01:44):

@Sean Is that potentially useful for boolean expression simplification?

view this post on Zulip Sean (May 05 2020 at 02:56):

oh heck no :)

view this post on Zulip 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).

view this post on Zulip 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: Oct 09 2024 at 00:44 UTC