[HN Gopher] Synthesizing optimal 8051 code with an SMT solver (2...
       ___________________________________________________________________
        
       Synthesizing optimal 8051 code with an SMT solver (2020)
        
       Author : pkkm
       Score  : 55 points
       Date   : 2022-12-10 17:39 UTC (5 hours ago)
        
 (HTM) web link (lab.whitequark.org)
 (TXT) w3m dump (lab.whitequark.org)
        
       | PaulHoule wrote:
       | Seems to me it would be better still the optimize the whole
       | calculate the rotate is a part of (maybe you don't really need
       | one of those rotates) but that's a lot tougher.
       | 
       | It is great to see SMT used for more real problems though!
        
         | mynameisash wrote:
         | I would love to see more practical applications of SMT,
         | particularly as intros to newbies.
        
           | __init wrote:
           | Check out angr [1], a symbolic execution engine, and claripy
           | [2], its frontend to SMT solvers like z3. Depending on your
           | background, I probably wouldn't describe angr as "for
           | newbies," but claripy is a very clean SMT interface!
           | 
           | [1] https://angr.io
           | 
           | [2] https://api.angr.io/claripy.html
        
           | c0742e9366 wrote:
           | The (freely available) book "SAT/SMT by Example" [1] shows
           | how a lot of different problems can be tackled with an SMT
           | solver. I highly recommend it!
           | 
           | [1] https://sat-smt.codes/
        
         | pkkm wrote:
         | That was my thought too. The author says that the memory usage
         | grows extremely quickly; I wonder if there's a way to reduce
         | it.
        
           | espadrine wrote:
           | Isn't that what DeepMind tried to circumvent by using
           | AlphaZero for AlphaTensor, to discover faster matrix
           | multiplication techniques?
        
             | pkkm wrote:
             | I think so. Their algorithms aren't known to be optimal
             | though, just better than the previous ones.
        
       ___________________________________________________________________
       (page generated 2022-12-10 23:00 UTC)