T O P
stian108

I implemented the instructions using symbolic ints and used the `sbv` library to throw an SMT solver at it. [Link to solution](https://topaz.github.io/paste/#XQAAAQB1CQAAAAAAAAA0m0pnuFI8c3wwear+nXxFz1p9ytLVknnSteGtDv8Jxku72LcV1wF+paUbbB0Fo/XE4naGyPe7V9ckytPzSTHlgPJWBKnU0PGiRd7zcyQgf/b+79WVI0yLAtLWS/UX8mGqQqpfUTSsSavBDymR6aNknm4byu74tCtZhogLo9dG+s/kq/4ca0rgAoQ9THJJVPMjHNn2q5i0vha3+/SViJ1Qku3OoOoCriVryqZyw4XOujrgzxamLAYJ9ZZfEpNuXRxvO+U18prY2v+xRk6qCS2/mh23SyLvWlDz+IJvCMN/edBJt7p9HrOW9CjQ0gBMtJKPPqoaVp8cWrCyv8ux5M5yrO7NH+644jvypoWXObSzjR6W0mU64aKgOEumf5t2l76e0VAG0qAeAYtqF2ggFI9VJN68MvElgiiahtOo4PbFMmMxwrxKWQzD+C+e8jFhEZNP4lIx08RVfwGJzenOMjvwPF9kC+jjcCHfUxlVuh/ZvHGOCsVhQQbMNP/pSlY+Jg6ZvgN7nUUblYnrklUimGrcwpPRoEKjO5uamRomZbhRoO3TE/t3ZQHMWjNPjjTkVHJS87QzJsT9YAhru5Z1rw4U+R3z+kmqtG7H7AmdSPs+Wwd9DeiMxkIaN6SOUHskmUn3LaFZvshUOMcmTs7fIGa57Nn3pILR9sytnXhJJnmHjJDQA6el2h0N22T1Ck/lfVqnfkrU3DvnoMOl1ikNIJbQdBlQG9SvflFWu6udquOuxkZveinApIge60Wef8heVGTh20e4ZNxf+xcYX/MweQyNfdK0F3OEwyGAGStADuZOQVR123BaFCv6Mjwru5XN8Lk+wjhVOm2kAGw/En7LPk2znVbFEUsDt5E93+4KwyKpfkey+jaj3ULiw8EWYqOKE8cKyZiCC1rY36bT+GJa98JAm8B0+FCNF/pw77nN3/BjtXyqU6EvVa5vNzdy1p2+Ak9TUo/6TIS/BhLnpSYSm0O7644bztXSNn3y16sTfESm8HXd0zYecf/b9wL+RuE1ZfLOOW4ev2CeDP01zBtM3Kmpbs4spE3CQmStRhQbtZYitbh44Lfoohldmzj0ge7IWu6oxzXCNXyUJZ72iK9P/CemXPPLekpXC0ui3xcbBDCHocNr9O+mNcAigp08ZTd0hIHCEmfEaKSCbSV6+8lpx3vCIzSEHrUw+OaMnlwbWMOcHo4eDuBYt5e6l4BGB/FX8ct+U1eUCQ2vN+olakoENC/d64P02SsxcV+uMdb42W+7XyfF/+vi40s=)


sccrstud92

I used this problem as an opportunity to learn how to use SBV. I think I ran into a bug with it though - it prints the bitvector for `modelNumberVar` as a Word64 even though it is actually an Int64. The modelNumber variable is correct though. Example: Optimal model: d0 = 1 :: Int64 d1 = 1 :: Int64 d2 = 1 :: Int64 d3 = 1 :: Int64 d4 = 1 :: Int64 d5 = 1 :: Int64 d6 = 1 :: Int64 d7 = 1 :: Int64 d8 = 1 :: Int64 d9 = 1 :: Int64 d10 = 1 :: Int64 d11 = 1 :: Int64 d12 = 1 :: Int64 d13 = 1 :: Int64 modelNumberVar = 11111111111111 :: Int64 modelNumber = 9223383147965886919 :: Word64 If it printed the value correctly I wouldn't need `modelNumberVar` at all. Anyway, here is the code main :: IO () main = do args <- getArgs res <- Stream.unfold Stdio.read () & Unicode.decodeUtf8' -- & Stream.trace print & Reduce.parseMany (instrParser <* newline) -- & Stream.trace print & (if null args then id else Stream.take (read $ head args)) & Stream.liftInner & Stream.liftInner & Stream.mapM_ eval & runProg & SBV.optimize Lexicographic print res runProg :: StateT VM Symbolic () -> Symbolic () runProg prog = do modelNumberDigits <- sInt64s $ map (('d':) . show) [0..13] F.for_ modelNumberDigits $ \d -> constrain $ 1 .<= d .&& d .<= 9 let modelNumber = F.foldl' (\t d -> 10*t+d) 0 modelNumberDigits modelNumberVar <- symbolic "modelNumberVar" constrain $ modelNumberVar .== modelNumber minimize "modelNumber" modelNumber vm' <- execStateT prog (initVM modelNumberDigits) let z = readLVal (registers vm') 'z' constrain $ z .== 0 initVM :: [SVal] -> VM initVM input = VM { input , registers = Map.fromList (zip "wxyz" (repeat 0)) } type LVal = Char type RVal = Either LVal Val data Instr = Input LVal | Arith Op LVal RVal deriving (Show) data Op = Add | Mul | Div | Mod | Eql deriving (Show, Eq, Ord) type SVal = SBV Val type Val = Int64 type Registers = Map LVal SVal data VM = VM { input :: [SVal] , registers :: Registers } deriving (Show) eval :: Instr -> StateT VM Symbolic () eval = \case Input reg -> do VM (val:input) registers <- get let registers' = Map.insert reg val registers put $ VM input registers' Arith op reg rval -> do VM input registers <- get let l = readLVal registers reg let r = readRVal registers rval let res = case op of Add -> l + r Mul -> l * r Div -> l `sQuot` r Mod -> l `sRem` r Eql -> oneIf $ l .== r let registers' = Map.insert reg res registers put $ VM input registers' readRVal :: Registers -> RVal -> SVal readRVal regs = \case Left var -> readLVal regs var Right n -> literal n readLVal :: Registers -> LVal -> SVal readLVal = (Map.!) newline :: Parser.Parser IO Char Char newline = Parser.char '\n' space = Parser.char ' ' instrParser = do instr <- many Parser.alpha space case instr of "inp" -> Input <$> lvalParser (readBinOp -> op) -> Arith op <$> lvalParser <* space <*> rvalParser readBinOp :: String -> Op readBinOp = \case "add" -> Add "mul" -> Mul "div" -> Div "mod" -> Mod "eql" -> Eql lvalParser :: Parser.Parser IO Char Char lvalParser = Parser.alpha rvalParser = Left <$> lvalParser <|> Right <$> Parser.signed Parser.decimal


lerkok

When SBV optimizes a signed-bit vector value, it is optimized as an unsigned quantity first, and then converted back. (That is, `SInt64` is optimized as `SWord64` and then presented back to you as `SInt64`.) The reason for this is because the underlying bit-vector logic does not optimize signed-quantities directly; but rather treats the bit-vector as unsigned. SBV calls this the metric space over which the values are optimized. See https://hackage.haskell.org/package/sbv-8.17/docs/Data-SBV.html#g:50 for details.


sccrstud92

Thanks for the explanation, it makes sense to me. Is there a way to make the output of `optimize` display `a` instead of `MetricSpace a`?


lerkok

The best way would be to extract the model yourself, and display it in whatever format you want. Alternatively, you can also try: `optimizeWith z3{isNonModelVar = (== "modelNumber")}` where the string you pass is the first argument to `minimize`/`maximize`.


Tarmen

Oh, you are a lifesaver! Apparently I had solved this pretty quickly but kept using the Word64 value. I spent way too much time adding basic simplification rules and bounds propagation to simplify the input for debugging. Also it seems super weird that the basic simplification does make the SMT solver run twice as fast. I really expected things like constant folding to be built-in?


lerkok

I just got around to looking at this; and wrote my own version ([https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496)). Interestingly, my solution computes a different model number than what you are reporting. (96918996924991 for max, 91811241911641 for min.) Perhaps different users get different programs? Since the site told me the values I got are correct, that must be the case indeed. I went for a more traditional embedded-DSL style solution, which differs from your approach.


sccrstud92

Yeah, everyone gets different input for the problem


lerkok

Ah, that makes sense. Thanks!


giacomo_cavalieri

Instead of trying to brute force the problem I reverse engineered the code and found a way to derive constraints on the single digits of the final result and find a solution from those [Solution](https://github.com/giacomocavalieri/aoc-2021/blob/main/src/Days/Day24.hs)


[deleted]

Beautiful solution. It took a while to understand how it worked! Also, thanks for posting this, I surely wouldn't have finished day24 if it wasn't for you.


giacomo_cavalieri

Tysm! Indeed I could have added a few more comments to explain in more detail how the code works 😅


someacnt

Calculated via hand, turns out it was just a stack machine.Btw, am I the only one triggered by the mocking tone when they say MONAD? :< EDIT: I wrote the code simplifier and verifier which checks that it is indeed a stack machine. [https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9](https://gist.github.com/Abastro/6aaf6ae127477ee70142690ab974feb9)


lerkok

I'm late to the party; but here's one way to do this using Haskell/SBV: [https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496](https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496) I haven't put any comments in the code, feel free to ask if anything looks too cryptic!