This post will show a solution to Advent of Code 2021 day 8, "Seven Segment Search" in F#. Part 1 shows the analysis supporting this solution.

Domain Model Types

First, some types to represent our problem domain, and their associated helper functions:

/// Represent individual segments in a 7-segment display by location
type Segment = TT | TL | TR | MM | BL | BR | BB

module Segment =
    let all : Segment list = [ TT ; TL ; TR ; MM ; BL ; BR ; BB ]


/// Digits that can be displayed on a single 7-segment display
type Digit = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9

module Digit =
    /// All digits in a list in order from smallest to largest
    let all : Digit list = [D0 ; D1 ; D2 ; D3 ; D4 ; D5 ; D6 ; D7 ; D8 ; D9]

    /// Numeric value of a digit        
    let intValue digit : int =
        match digit with
        | D0 -> 0
        | D1 -> 1
        | D2 -> 2
        | D3 -> 3
        | D4 -> 4
        | D5 -> 5
        | D6 -> 6
        | D7 -> 7
        | D8 -> 8
        | D9 -> 9

    /// The segments used to display a digit
    let segments digit : Set<Segment> =
        match digit with
        | D0 -> [| TT; TL; TR;     BL; BR; BB |]
        | D1 -> [|         TR;         BR     |] 
        | D2 -> [| TT;     TR; MM; BL;     BB |]
        | D3 -> [| TT;     TR; MM;     BR; BB |]
        | D4 -> [|     TL; TR; MM;     BR     |]
        | D5 -> [| TT; TL;     MM;     BR; BB |]
        | D6 -> [| TT; TL;     MM; BL; BR; BB |]
        | D7 -> [| TT;     TR;         BR     |]
        | D8 -> [| TT; TL; TR; MM; BL; BR; BB |]
        | D9 -> [| TT; TL; TR; MM;     BR; BB |]
        |> Set.ofArray

    (* Pre-compute the table for 'withSegmentCount' *)
    let _digitsByNumberOfSegments = 
        all |> List.groupBy (segments >> Set.count) |> Map.ofList

    /// Returns a list of the digits that use the specified number of segments
    let withSegmentCount n : Digit list =
        _digitsByNumberOfSegments
        |> Map.tryFind n
        |> Option.defaultValue List.empty

• Although we could just as well use the int type directly for digits, using a union type lets the compiler check our match expressions for exhaustiveness - we can't forget a digit
  • In a language with range types (e.g. Ada), that could be a less-verbose option.
• The function Digit.withSegmentCount could use a match expression instead, but since we can calculate the result using Digit.segments, I decided to compute a map and use a lookup instead.

Unique Assignment

Next, implementing the unique assignment constraint for our segments:

1. Initially, we assume any signal line could correspond to any segment
2. When we determine that a particular signal line matches a particular segment, we "assign" that signal to that segment and remove it as a possibility for all other segments

module EnforceUniqueAssignment =
    type AssignmentState =
        { assigned : Map<Segment, char>
        ; unknown : Map<Segment, Set<char>>
        }

    let ignoreKey fn _k v = fn v    

    let isSolved (state : AssignmentState) : bool =
        Map.isEmpty state.unknown && 
        Map.count state.assigned = 7

    /// assign a value to a segment
    /// (1) adds the segment and its value to the 'assigned' table
    /// (2) removes the value as a possibility from remaining segments with an unknown signal
    let assign (state : AssignmentState) (segment : Segment) (value : char) : AssignmentState =
        
        let removeIt = ignoreKey (Set.remove value)
        
        { assigned = Map.add segment value state.assigned
        ; unknown = Map.map removeIt state.unknown
        }

    /// search table of unknown segments for those with one remaining possibility
    let rec assignSingletons (state: AssignmentState) : AssignmentState =
        // helper functions for working with sets
        let hasOneValue (s : Set<'a>) =
            (Set.count s) = 1

        let getOnlyValue(s : Set<'a>) =
            Set.toList s |> List.head

        // check the 'unknown' table for segments that have only one possible value.
        let haveOneValue, others =
            Map.partition (ignoreKey hasOneValue) state.unknown

        if Map.isEmpty haveOneValue then
            // BASE case - all segments we know the exact value for are already in
            // the 'assigned' table, there are no segments with one possible value
            // in the 'unknown' table and we don't need to change anything.
            state
        else
            // RECURSIVE case - at least one segment we can assign the value for            
            haveOneValue
            // 1) convert sets of one value to just that value
            |> Map.map (ignoreKey getOnlyValue)
            // 2) move segments with one value from the 'unknown' table to the 'assigned' table
            |> Map.fold assign { state with unknown = others }
            // 3) re-check the updated table for new segments that may now have only one value
            |> assignSingletons

    let constrainAndAssign state constraintFn input =
        let reduced = { state with unknown = constraintFn state.unknown input }
        let assigned = assignSingletons reduced
        assigned

    let constrainWithInputs initial constraintFn inputs =
        let rec loop state remainingInputs =
            if isSolved state then
                state
            else
                match remainingInputs with
                | head::tail ->
                    let state' = constrainAndAssign state constraintFn head
                    loop state' tail
                | _ -> failwith "out of inputs to constrain with!"
        
        loop initial inputs 

1. For simplicity I did not make the AssignmentState record type generic - it is straightforward to do so but makes the type signatures throughout the module much less clear
2. Similarly, the isSolved function is specific to our problem domain. To make the module reusable, it would need to be passed as a parameter to the constrainWithInputs function
3. constrainWithInputs is structurally very similar to List.fold, with the addition of terminating early (not processing the entire list of inputs) when all segments are assigned (i.e. isSolved returns true).
4. The type signature for the constraintFn parameter is as follows: (Map<Segment, Set<char>> -> 'a -> Map<Segment, Set<char>>). The intent is to take in an AssignmentState.unknown table and some input, and use that input to reduce the number of possible values for one or more segments in the table, returning the new table.

Implementing constraintFn

Although we've implemented unique assignment above, we still need to implement a way to reduce the number of possible values for what signal lines correspond to what segments. By applying this repeatedly, we'll eventually find a segment with only one possible value and trigger our unique assignment constraint.

As discussed previously, we can use the fact that digits with the same number of segments use some segments in common to do this.

/// Look for digits that use the same number of segments as there are signals in the given pattern,
/// find any segments used in common by all of those digits, then
/// remove any signals not in the pattern as possible values for those segments.
let reducePossibleValues (segmentsToPossibilies : Map<Segment, Set<char>>) (pattern : Set<char>) : Map<Segment, Set<char>> =
    // get the digits that might be represented by this pattern, based solely on the number of signals/segments it uses
    let numberOfSegments = Set.count pattern
    let possibleDigits = Digit.withSegmentCount numberOfSegments

    // get the segments that are common to all those digits
    let segmentsInCommon = 
        possibleDigits
        |> List.map Digit.segments
        |> Set.intersectMany

    segmentsToPossibilies
    |> Map.map (fun segment possibleValues ->
        // if this map entry is for one of those segments, remove any possible values that aren't in the pattern
        if Set.contains segment segmentsInCommon then
            Set.intersect possibleValues pattern
        // (otherwise skip it)
        else
            possibleValues
    )

This function then slots neatly into the constraintFn parameter of EnforceUniqueAssignment.constrainWithInputs.

Processing problem inputs

Next, these types are used to represent the problem input.

Store each string from a line of input as a set of characters, since

1. signals don't repeat in a pattern,
2. the order of signals doesn't matter, and
3. this lets us use set intersection built-in to the standard library

type Pattern = Set<char>

module Pattern =
    let toString p =
        p |> Set.toArray |> Array.sort |> String
    
    let ofString (s : string) =
        s.ToCharArray() |> Set.ofArray

Then we have helper functions to convert to and from strings, for printing and parsing respectively.

Each line of the problem input is independent and has two halves:

1. One pattern for each of the digits 0-9
2. Four additional patterns representing the current value, which we need to decode to a number

So we can represent a line of input as a record with a field/member for each half:

type Entry = 
    { examples : Pattern list
    ; current : Pattern list
    }

module Entry =
    
    let parse (line : string) : Entry =
        
        let toPatternList (text : string) : Pattern list =
            text.Split(' ', StringSplitOptions.None)
            |> Array.map Pattern.ofString
            |> Array.toList

        let halves = line.Split('|', StringSplitOptions.TrimEntries)
        
        { examples = toPatternList halves[0]
        ; current = toPatternList halves[1]
        }

    let toString (e : Entry) : string =
        let formatPatterns (ps : Pattern list) : string =
            ps
            |> List.map Pattern.toString
            |> String.concat ", "

        let fmtdExamples = formatPatterns e.examples
        let fmtdCurrent = formatPatterns e.current
        sprintf "Entry{ex= %s ; now= %s}" fmtdExamples fmtdCurrent

    let decode (entry : Entry) : Digit list =
        let segmentsToPossibilities =
            Segment.all
            |> List.map (fun s -> (s, Set.ofList ['a' .. 'g']))
            |> Map.ofList

        let initialState : EnforceUniqueAssignment.AssignmentState = 
            { assigned = Map.empty
            ; unknown = segmentsToPossibilities
            }

        let characterForSegment : Map<Segment, char> = 
            EnforceUniqueAssignment.constrainWithInputs initialState reducePossibleValues entry.examples
            |> fun r -> r.assigned
        
        let stringForDigit (d : Digit) : string =
            Digit.segments d
            |> Set.map (fun s -> Map.find s characterForSegment)
            |> Pattern.toString

        let digitForString : Map<string, Digit> =
            Digit.all
            |> List.map (fun d -> (stringForDigit d, d))
            |> Map.ofList

        let displayValues =
            entry.current
            |> List.map Pattern.toString
            |> List.map (fun str -> digitForString[str])

        displayValues

The helper functions include the usual for converting to and from strings, but also Entry.decode - this brings all our earlier functions together to solve a single line of problem input. It determines what segments each letter corresponds to using the example patterns, and uses that to determine each of the 4 digits on the "current display".

1. Create an initial state record where any segment could be represented by any character
2. Use our functions constrainWithInputs and reducePossibleValues to create an exact mapping from each segment to the character/signal that it corresponds to
3. Use the map from step 2 to build a second map, from each digit to the pattern/string that represents that digit for the current signal configuration
4. Use the map from step 3 to match the currently displayed patterns to the digits they represent

Solving the full problem

Lastly, we just need to read our problem inputs, decode them, and use the decoded values to answer the questions posed by the Advent of Code challenge:

// reading lines of input as strings
let standardInput =
    fun _ -> Console.In.ReadLine()
    |> Seq.initInfinite
    |> Seq.takeWhile ((<>) null)


// read and decode problem inputs
let decodedEntries = 
    standardInput 
    |> Seq.map (Entry.parse >> Entry.decode)
    |> Seq.toList


// how many times to the digits 1, 4, 7, or 8 appear?
let part1 (digits) =
    let count1478 digit =
        match digit with
        | D1 | D4 | D7 | D8 -> 1
        | _ -> 0
    List.sumBy count1478 digits

// what do you get if you add up all the output values?
let part2 (digits) =
    digits
    |> List.map Digit.intValue
    |> List.map (sprintf "%d")
    |> String.concat ""
    |> int

let part1solution = decodedEntries |> List.sumBy part1
let part2solution = decodedEntries |> List.sumBy part2
printfn "Part 1: %d | Part 2: %d" part1solution part2solution

I prefer to have my programs read from standard input rather than directly from a file, so I can pipe input to them instead.

You can see a complete script as a Gitlab Snippet. With the dotnet command line tools, running it looks like this:

PS C:\Users\mrsei\source\advent of code\2021> gc .\inputs\day8\full.txt | dotnet fsi .\seven-segment-search.fsx
Part 1: *** | Part 2: *******

Related

If you found this at all interesting, you may also like this writeup by Dimitri Bohlender:

Solving the "Seven Segment Search" Puzzle with Z3

They express the problem as a series of logical constraints, with a mathematical formalization that can be used with a generic SMT solver. This is a much more rigorous characterization of the problem, and teaches a lot about SMT/SAT solvers!