The Three-Sat Problem - LA CTF 2025 Reverse Engineering Writeup

Category: Reverse Engineering Difficulty: 180 points Solves: 97 Flag: lactf{is_the_three_body_problem_np_hard} Solved by: Smothy @ 0xN1umb

"They said P != NP. Z3 said hold my beer."

Challenge Description

I have this groundbreaking sci-fi novel idea where it's proven that P=NP then suddenly all of cryptography and subsequently all of society collapses- hey wait why are you leaving I haven't finished pitching my idea yet

Classic aplet123 energy. We're given a single stripped ELF binary called three_sat_problem. The name is a dead giveaway - this is going to be a Boolean satisfiability challenge. Time to make an NP-complete problem feel very P.

TL;DR

Binary takes 1279 binary digits as input, evaluates them against a massive 3-SAT formula baked into the assembly, and spits out the flag if all clauses are satisfied. We used angr's symbolic execution (powered by Z3) to solve the entire thing in ~2 seconds. SAT solvers go brrr.

Initial Recon

Standard stripped PIE binary, 82KB. Nothing crazy on the surface. Let's run it and see what happens:

Three strings tell the whole story:

• "Have you solved the Three-Sat Problem?" - the prompt
• "Please be serious..." - rejection
• "Incredible! Let me get the flag for you..." - victory

So we need to provide the right input. Let's figure out what "right" means.

Step 1: Reversing Main - Input Format

Disassembling main() at offset 0x1090 reveals the input validation:

The input requirements are crystal clear:

1. Reads up to 0x500 (1280) bytes with fgets
2. Strips the newline with strcspn
3. Checks strlen == 0x4FF (1279) - must be exactly 1279 characters
4. Validates each character is either '0' (0x30) or '1' (0x31)

So our input is 1279 boolean variables represented as ASCII 0s and 1s. This is literally a SAT problem - each character is a variable assignment.

Step 2: The SAT Checker - 15,000 Lines of Boolean Hell

After input validation, main calls the SAT checker function at 0x1289:

This function is an absolute unit. 15,302 lines of disassembly. 8,653 boolean operations. The structure is textbook 3-SAT:

1. Load phase: Read individual input bytes (variables) from the buffer, optionally negate them (NOT), mask to 1 bit (AND 1), and store as literals on the stack
2. Clause evaluation: OR three literals together per clause, AND all clause results together
3. Return: 1 if all clauses satisfied, 0 otherwise

For the homies who haven't touched computational complexity theory: 3-SAT is the OG NP-complete problem. Given a formula in conjunctive normal form (AND of OR-clauses, each with 3 literals), find a variable assignment that makes it true. In the worst case, brute force takes 2^1279 attempts. That's... a lot.

But we're not brute forcing. We have Z3.

Step 3: Angr + Z3 - Let the Machines Think

Instead of extracting all the SAT clauses manually (lol no), we use angr - a symbolic execution framework that represents program inputs as symbolic variables and uses Z3 to solve for values that reach a target address.

The strategy:

1. Start at 0x1110 (right before the SAT checker call)
2. Place 1279 symbolic bytes in the input buffer at 0x15060
3. Constrain each byte to 0x30 ('0') or 0x31 ('1')
4. Set rbp to point at the buffer (as main does)
5. Tell angr: find 0x1135 (success), avoid 0x1124 (failure)
6. Let Z3 solve the constraints

import angr
import claripy

proj = angr.Project('./three_sat_problem', auto_load_libs=False)
base = proj.loader.main_object.min_addr

success_addr = base + 0x1135  # "Incredible! Let me get the flag..."
fail_addr    = base + 0x1124  # "Please be serious..."
buf_addr     = base + 0x15060 # Input buffer (global BSS)

# Start right before the SAT checker call
state = proj.factory.blank_state(addr=base + 0x1110)

# 1279 symbolic bytes constrained to '0' or '1'
sym_input = claripy.BVS("input", 8 * 1279)
state.memory.store(buf_addr, sym_input)

for i in range(1279):
    byte = sym_input.get_byte(i)
    state.solver.add(claripy.Or(byte == 0x30, byte == 0x31))

state.regs.rbp = buf_addr
state.regs.rsp = 0x7fff0000

simgr = proj.factory.simulation_manager(state)
simgr.explore(find=success_addr, avoid=fail_addr)

if simgr.found:
    solution = simgr.found[0].solver.eval(sym_input, cast_to=bytes)
    with open("solution.txt", "wb") as f:
        f.write(solution)
    print(f"Solved! {len(solution)} bytes")

Result: Solution found in ~2 seconds. Z3 ate those 1279 variables and hundreds of clauses for breakfast.

Step 4: The Solution

1279 boolean values. Each green cell is a 1 (TRUE), each dark cell is a 0 (FALSE). This assignment satisfies every single clause in the 3-SAT formula.

Step 5: Flag Construction

The binary doesn't just check the SAT solution - it derives the flag from it. After validation passes, there's a loop at 0x1155 that:

1. Reads 320 entries from a lookup table (offsets into the input buffer)
2. Extracts one bit from each referenced input position
3. Packs 8 bits into each byte
4. Produces a 40-byte string = the flag

The Flag

lactf{is_the_three_body_problem_np_hard}

A beautiful reference to Cixin Liu's The Three-Body Problem + the NP-hardness of 3-SAT. The challenge author is clearly a person of culture.

The Solve Script

"""
The Three-Sat Problem - LA CTF 2025
Reverse Engineering - 180 points
Solver by Smothy @ 0xN1umb

Angr symbolic execution to solve a 3-SAT instance
encoded in x86 assembly (1279 boolean variables).
"""

import angr
import claripy

proj = angr.Project('./three_sat_problem', auto_load_libs=False)
base = proj.loader.main_object.min_addr

# Key addresses (PIE-relative, angr rebases to 0x400000)
SUCCESS  = base + 0x1135  # "Incredible! Let me get the flag for you..."
FAIL     = base + 0x1124  # "Please be serious..."
BUF_ADDR = base + 0x15060 # Global input buffer
START    = base + 0x1110  # Right before call to SAT checker

# Create blank state at the start point
state = proj.factory.blank_state(addr=START)

# Symbolic input: 1279 bytes, each constrained to '0' or '1'
sym_input = claripy.BVS("input", 8 * 1279)
state.memory.store(BUF_ADDR, sym_input)

for i in range(1279):
    byte = sym_input.get_byte(i)
    state.solver.add(claripy.Or(byte == 0x30, byte == 0x31))

# Set up registers as main would have them
state.regs.rbp = BUF_ADDR
state.regs.rsp = 0x7fff0000

# Explore: find success, avoid failure
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=SUCCESS, avoid=FAIL)

if simgr.found:
    solution = simgr.found[0].solver.eval(sym_input, cast_to=bytes)
    with open("solution.txt", "wb") as f:
        f.write(solution)
    print(f"[+] Solution found! ({len(solution)} bytes)")
    print(f"[+] Run: cat solution.txt | ./three_sat_problem")
else:
    print("[-] No solution found :(")

The Graveyard of Failed Attempts

1. First angr attempt with full stdin simulation - angr's SimFile stdin API kept throwing TypeError about len(). Turns out the write method changed in newer angr versions. Wasted time fighting the API.

2. Starting from entry_state - angr explored zero states. The full program startup path with fgets/strlen/strcspn was too complex for angr to handle cleanly with symbolic stdin.

3. The fix: blank_state at the right address - Skip all the input I/O, start right at the validation call with symbolic memory already in place. Solved instantly. Sometimes the best approach is skipping the boring parts.

Key Takeaways

1. 3-SAT is THE classic NP-complete problem - recognizing it from the challenge name saved massive time. No need to reverse 15,000 lines of assembly when you know it's SAT.

2. Angr's blank_state is your friend - when the program's I/O handling is annoying, just skip it. Set up memory and registers manually and start where the interesting logic begins.

3. Z3 handles real-world SAT instances easily - despite 3-SAT being NP-complete in theory, practical instances (even with 1279 variables) are often solved in seconds by modern SAT solvers. The theoretical worst case almost never happens.

4. The flag is derived from the solution - the SAT assignment isn't arbitrary. Specific bits are extracted to construct the flag, meaning there's likely a unique solution (or at least the flag-relevant bits are fully constrained).

5. Read the challenge name - "Three-Sat Problem" literally tells you what it is. CTF authors are usually honest about the category.

Tools Used

• objdump - Disassembly and initial analysis
• strings / file / checksec - Standard recon
• angr + Z3 - Symbolic execution and SAT solving
• Python 3 - Gluing it all together
• Way too much caffeine

Writeup by Smothy from 0xN1umb team. P may not equal NP, but angr doesn't read theory papers. GG.