is it actually less work than just doing it manually? probably not. but we're doing it anyway

fun racket fact of the day:

you can bind the empty identifier. no, really

the pipe | is the escape character for symbols, so eg |5| is the symbol 5, rather than the number 5
so what happens if we use ||?

$ racket
Welcome to Racket v7.9 [bc].
> (define || "meow")
> (displayln ||)
meow

🤔

> (namespace-variable-value (string->symbol ""))
"meow"

yeah.

anyway

my current bit is going to be swapping the title and subtitle of posts, just for fun

i wanted to demo a cool thing you can do when you're too lazy to solve logic puzzles. the example here is a puzzle "icebreaker" from the previous teammate puzzle hunt: https://teammatehunt.com/puzzles/icebreaker

spoilers follow

.

..

...

....

here's the puzzle contents

MARTIN: "Before the party, let’s play a quick icebreaker. I’ll start. My three statements are:

• The five of us are, in no particular order, the person who lives in the first house, RAMSEY, the person who has a pet FERRET, the person who has a pet POODLE, and the person from KANSAS.
• TURNER and the person who owns WHALES live on opposite ends of the street.
• WALTER is from FRANCE, but doesn’t own a FERRET."

RAMSEY: "I’ll go next. My three statements are:

• MARTIN and the person from LONDON live on opposite ends of the street.
• SANDRA is from LONDON, but doesn’t own a FERRET.
• WALTER lives immediately to the left of me."

SANDRA: "I’ll go next. My three statements are:

• I own pet ROBINS.
• The person who owns WHALES lives two houses away from the person from FRANCE.
• WALTER is from TAIPEI."

TURNER: "I’ll go next. My three statements are:

• I am not from KANSAS.
• I was alone yesterday taking my TIGERS to the vet.
• RAMSEY’s pet ROBINS live three houses away from me.

WALTER: "I’ll go last. My three statements are:

• I met up yesterday with the person who has a POODLE and also the person who lives in the second house.
• The five of us are, in no particular order, me, SANDRA, the person who owns ROBINS, the person from MUMBAI, and the person from TAIPEI.
• TURNER is from KANSAS, and doesn’t live in the first house.

this is a bog standard logic puzzle and given the title "icebreaker" you can convince yourself that the theme of this icebreaker is "two truths and a lie" which implies that one of each set of 3 statements is false, and the other 2 are true

if you're familiar with this sort of thing you may be going straight to google sheets and making a logic grid but we can do better than that because it turns out that people have already made cool programs that automate the process of solving satisfiability problems so if we can convert all of this text into a giant boolean expression then feed it to a solver it should give us answers... and hopefully not unsat ...

to be honest my initial implementation of this problem was entirely booleans, which meant the code ended up being very large and very spaghetti and contained some very spaghet manual axioms that were necessary in the system before it arrived at a working solution. so i rewrote it, because it turns out there's a better way to represent the problem

we have the following categories of things

• names of people
• places they're from
• pets they own
• houses they live in on the street (in some order)

there are five items in each category, and the statements in the puzzle text provide some expressions over these that might be true or false
the representation i chose for a cleaner solution was

• houses are concrete numbers, 1-5
• everything else is a symbolic variable (what we're solving for to make the boolean expressions satisifiable) that holds a house number corresponding to it

this means we get basic axioms for free from integers and don't have to define them ourselves, which is a pain

anyway here's the setup

#lang curly-fn rosette

(require syntax/parse/define
         (for-syntax racket/syntax))

oh yeah we're going to be using rosette, a solver aided programming library for racket, just because we can

and we're using macros. you bet

;; house is represented by actual number
;; people, places, pets represented by symbolic variable
(define-for-syntax *data*
  '((name martin ramsey sandra turner walter)
    (place london kansas france taipei mumbai)
    (pet robins tigers whales ferret poodle)))

;; create a solver and define all the symbolic variables
(define-simple-macro (define-symbols/solver solver:id)
  ;; generate list of ids, bound to calling lexical context, with a syntax prop determining the
  ;; category
  #:with (ids ...) (for*/list ([row (in-list *data*)] [val (in-list (rest row))])
                     (syntax-property (format-id #'solver "~a" val) 'icebreaker:cat (first row)))
  ;; create the symbolic define expressions
  #:with (defs ...) (for/list ([id (in-list (syntax-e #'(ids ...)))])
                      #`(define-symbolic #,id integer?))
  ;; create initial constraints
  #:with (stmts ...) (let ([groups (group-by #{syntax-property % 'icebreaker:cat}
                                             (syntax-e #'(ids ...)))])
                       (append (for*/list ([grp (in-list groups)] [id (in-list grp)])
                                 ;; all in [1, 5]
                                 #`(void (solver (<= 1 #,id 5))))
                               (for/list ([grp (in-list groups)])
                                 ;; no two in the same category are equal
                                 #`(void (solver (mutually-exclusive #,@grp))))))
  (begin
    ;; incremental solver
    (define solver (solve+))
    defs ...
    stmts ...))

(define-symbols/solver inc)

this is the bulk of the setup. it generates all the variables and creates a new SMT solver by macro and helpfully adds some basic assertions to the solver: each symbolic variable should be 1-5 and no two variables in the same category should be equal (mutually-exclusive is a custom macro, that's coming up it's not that complicated)

;; helper for defining the statements of one person (2 true, 1 lie)
(define-simple-macro (define-statements solver:expr sfirst:expr ssecond:expr sthird:expr)
  (void
    (solver (or (and sfirst ssecond (not sthird))
                (and sfirst (not ssecond) sthird)
                (and (not sfirst) ssecond sthird)))))

this is a macro that defines a set of 2 truths and a lie made by a person in the puzzle text. it basically just expands the set of three statements to assert that there is some combination where one is false and two are true

;; helper for defining a mutually exclusive set of symbolic and concrete values
(define-simple-macro (mutually-exclusive options:expr ...)
  #:with (stxs ...) (for/list ([combo (in-combinations (syntax-e #'(options ...)) 2)])
                      #`(not (= #,(first combo) #,(second combo))))
  (and stxs ...))

;; helper for asserting that 2 houses are at a certain distance apart
(define-simple-macro (at-distance v1:expr v2:expr dist:expr)
  (= dist (abs (- v1 v2))))

this is the last bit of setup. there's the mutually-exclusive macro and a macro for defining that 2 houses are at a certain distance apart (this happens a few times)

now we make the assertions, transcribed from the text

;; the rules
;; martin
(define-statements inc

The five of us are, in no particular order, the person who lives in the first house, RAMSEY, the person who has a pet FERRET, the person who has a pet POODLE, and the person from KANSAS.

use the handy mutually-exclusive macro

  (mutually-exclusive 1 ramsey ferret poodle kansas)

TURNER and the person who owns WHALES live on opposite ends of the street.

"opposite ends" is the same thing as distance 4 apart, so we use that macro. also this asserts that the two people here are distinct, so that's another thing to add

  (and (at-distance turner whales 4) (not (= turner whales)))

WALTER is from FRANCE, but doesn’t own a FERRET.

this is relatively basic

  (and (= walter france) (not (= walter ferret))))

and so on for the rest of the statements

;; ramsey
(define-statements inc
  (and (at-distance martin london 4) (not (= martin london)))
  (and (= sandra london) (not (= sandra ferret)))

the next statement is about being "immediately to the left". we assume house numbers go left-to-right (this turns out to be correct) and thus walter's number is ramsey's minus 1

  (= walter (sub1 ramsey)))

;; sandra
(define-statements inc
  (= sandra robins)
  (at-distance whales france 2)
  (= walter taipei))

;; turner
(define-statements inc
  (not (= turner kansas))
  (= turner tigers)
  (and (= ramsey robins) (at-distance ramsey turner 3)))

;; walter
(define-statements inc

this next one is also a case for mutually-exclusive, where the speaker, the poodle, and 2 are mutually exclusive (if you read the statement carefully this makes sense)

  (mutually-exclusive walter poodle 2)

almost done..

  (mutually-exclusive walter sandra robins mumbai taipei)
  (and (= turner kansas) (not (= turner 1))))

whew that was a lot of statements

finally we print the answer (hopefully it's sat!!)

;; this increments the solver with trivial truth because that's what we need to get the
;; model out
;; the define-statement macro voids everything so you can't get the last result normally
;; whatever. don't yell at me pls
(define solution (inc #t))
(displayln solution)

and this is what it outputs

$ racket icebreaker.rkt 
(model
 [martin 3]
 [ramsey 2]
 [sandra 4]
 [turner 5]
 [walter 1]
 [london 4]
 [kansas 5]
 [france 3]
 [taipei 1]
 [mumbai 2]
 [robins 2]
 [tigers 5]
 [whales 1]
 [ferret 3]
 [poodle 4])

and there you go. logic puzzle solved. this lists the house numbers for each name, pet, and place where person is from

1. walter, whales, taipei
2. ramsey, robins, mumbai
3. martin, ferret, france
4. sandra, poodle, london
5. turner, tigers, kansas

if you evaluate the original statements with this solution, you'll find that the following end up true (and the rest false)

• martin: 1, 2 true
• ramsey: 2, 3 true
• sandra: 2, 3 true
• turner: 2,3 true
• walter: 1, 3 true

the solution checks out

(there's a final step to get the actual answer to this puzzle but i'm not going over it because it's not super relevant. exercise to the reader, or something,)

you can find the full code (concatenation of all these blocks) here: https://git.lain.faith/haskal/gist/src/branch/gist/racket/icebreaker/icebreaker.rkt

but was it worth it?

haha no, but the solution is still interesting imo

manually solving this is probably a lot faster than writing out this SMT solver code and fixing the bugs if it's unsat or underconstrained. but there's of course also overhead in the macros and such for the code here that, while they took a bit to initially write here, could probably be reused for other einstein-type puzzles. maybe making a full logic puzzle assistance program based on SMT could be useful for future puzzlers 😛🦈

tune in next week for when i hopefully write another blog post because i rly should be writing stuff more than like, once every 2 months tbh