Tomasz Węgrzanowskitaw.hashnode.dev·Jan 1, 2023Break XOR Cipher with Z3In previous post, I showed how to break Caesar cipher with Z3. This wasn't really all that exciting as Caesar cipher has only 26 possibilities, so it's triival to break with brute force, and you can even just display all possible answers and choose t...Discuss·52 readsz3
Tomasz Węgrzanowskitaw.hashnode.dev·Dec 31, 2022Break Caesar Cipher with Z3Z3 is usually given a list of hard constraints, and told to solve them, but it can do quite a few more things. Let's use it unconventionally and break Caesar cipher. The Challenge The following plaintext from Wikipedia: In cryptography, a Caesar cip...Discuss·38 readsRuby
Kamil Gierach-Pacanekblog.cyberethical.me·Nov 23, 2022Solving Equations Like A ProBackground On October I have participated in MSHP CTF and one of the challenges intrigued me so much that I promised myself to create a separate article on that. Challenge Following screen is my recreation of the challenge. Original application made...Discuss·1.4K readsz3
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 16, 2022Open Source Adventures: Episode 74: Crystal Z3 Solver for Light Up PuzzleThis is the final episode with Crystal Z3 solvers, at least for now. In previous episode I showed how to solve Lights Up puzzle with math, now it's time to write a Crystal Z3 solver. Light Up (Akari) is a simple puzzle with following rules: there's ...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 15, 2022Open Source Adventures: Episode 73: How to solve Light Up Puzzle with mathLight Up (Akari) is a simple puzzle with following rules: there's a grid of cells some cells are wall cells your task is to place light bulbs in some of the cells light spreads horizontally and vertically from light bulbs, but it doesn't pass throug...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 10, 2022Open Source Adventures: Episode 72: Crystal Z3 Solver for Dominosa PuzzleDominosa is a puzzle with simple rules: there's a grid filled with numbers you need to pair those numbers into dominos each domino needs to be different As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 9, 2022Open Source Adventures: Episode 71: Improving Crystal Z3 ShardWhile writing various puzzle game solvers in Crystal Z3 I discovered two big issues: I frequently needed .reduce chains of +/*/and/or with special case for empty arrays Model#[] returned untyped result (Expr) even though its exact type is statically...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 6, 2022Open Source Adventures: Episode 70: Crystal Z3 Solver for Nonograms PuzzleNonograms is one of more popular puzzles. there's a grid of cells, you need do fill some of them each row and each column has some hints, each being a list of numbers a hint like "2 5 3" means the row (or column) has three groups of filled cells - a...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 6, 2022Open Source Adventures: Episode 69: Crystal Z3 Solver for Aquarium PuzzleAquarium is a puzzle with following rules: there's a grid of cells, belonging to various water containers each cell can contain water or not each container is filled to some level, that is - if a cell in a container has water, then every cell in the...DiscussOpen Source Adventurescrystal
Tomasz Węgrzanowskitaw.hashnode.dev·Jul 4, 2022Open Source Adventures: Episode 68: Crystal Z3 Solver for Switches PuzzleThis time something a bit different. I've seen variants of this puzzle as a minigame in a lot of hidden object games, but I haven't really seen it standalone anywhere. Here's the puzzle: there's a bunch of light bulbs, each connected by lines to som...DiscussOpen Source Adventurescrystal