CSP Solver

A Constraint Satisfaction Problem (CSP) Solver implemented as a Spring Boot microservice. All algorithms are implemented from scratch without external CSP libraries.

Demo

Start the app and open http://localhost:8080/visualize.html to watch the backtracking search solve N-Queens live: queens appear and retract as the solver assigns and backtracks, with node and backtrack counters streaming over the WebSocket.

Features

• Backtracking Search with a generic constraint model and pluggable heuristics
• Forward Checking propagation during search, with trailing-based rollback
• Arc Consistency (AC-3) preprocessing for domain reduction
• Variable Ordering Heuristics: MRV, Degree, MRV+Degree, Dom/WDeg (conflict-directed, learned weights)
• BitSet-backed domains with O(1) membership and cheap checkpoint/rollback
• Built-in Problems (REST endpoints): N-Queens, Sudoku, Graph Coloring, Cryptarithmetic
• Min-conflicts local search path for large N-Queens
• WebSocket streaming of live search progress
• REST API with OpenAPI/Swagger documentation
• Docker Support for containerized deployment

Performance

The solver runs two strategies for two regimes.

Systematic backtracking (complete search: forward checking + MRV/Degree, BitSet domains, trailing rollback). Measured on this machine, best of several runs:

Problem	Time	Search nodes
8-Queens	< 1ms	75
100-Queens	~15ms	185
200-Queens	~8s	~640,000
Sudoku (hard)	~65ms	~8,700

Backtracking N-Queens is instance-sensitive: some sizes (100, 1000) fall into a solution on the first greedy descent, while others (200, 500) thrash under natural value ordering. Roughly N <= ~150 is comfortable; 500 exceeds the practical ceiling for systematic search and is the regime the local-search path serves.

The trailing rollback (only the domains a node actually mutates are snapshotted and restored, rather than copying the full domain map per node) roughly halves per-node cost on rollback-heavy searches: 100-Queens 50ms to 22ms and 200-Queens 16.4s to 8.1s on the identical search tree.

Min-conflicts local search (used for large N-Queens, N >= 50, via the REST endpoint). This places 1000 queens in ~15ms. It is incomplete: it cannot prove unsatisfiability or enumerate all solutions, which is why the systematic solver remains the default for small N and exact queries.

Quick Start

Prerequisites

• Java 21+
• Maven 3.8+

Run with Maven

# Clone and build
mvn clean package -DskipTests

# Run the application
mvn spring-boot:run

Run with Docker

# Build and run with Docker Compose
docker-compose up --build

The API will be available at http://localhost:8080

API Reference

Swagger UI

Interactive API documentation is available at:

• Swagger UI: http://localhost:8080/swagger-ui.html
• OpenAPI Spec: http://localhost:8080/api-docs

Endpoints

Problems

Method	Endpoint	Description
GET	/api/v1/problems	List available problems
POST	/api/v1/problems/nqueens	Solve N-Queens problem
GET	/api/v1/problems/nqueens/{n}	Quick solve N-Queens
POST	/api/v1/problems/sudoku	Solve Sudoku puzzle
POST	/api/v1/problems/graph-coloring	Solve graph k-coloring
POST	/api/v1/problems/cryptarithmetic	Solve a cryptarithmetic puzzle (e.g. SEND+MORE=MONEY)

Benchmarks

Method	Endpoint	Description
GET	/api/v1/benchmark/nqueens	Benchmark N-Queens solver
GET	/api/v1/benchmark/nqueens/{n}	Benchmark specific size
GET	/api/v1/benchmark/compare-heuristics	Compare heuristics

Example Requests

Solve N-Queens

curl -X POST http://localhost:8080/api/v1/problems/nqueens \
  -H "Content-Type: application/json" \
  -d '{"n": 8}'

Response:

{
  "status": "SATISFIABLE",
  "satisfiable": true,
  "solutionCount": 1,
  "solutions": [{"Q0": 0, "Q1": 4, "Q2": 7, "Q3": 5, "Q4": 2, "Q5": 6, "Q6": 1, "Q7": 3}],
  "metrics": {
    "nodesExplored": 113,
    "backtracks": 37,
    "elapsedTimeMs": 2
  }
}

Solve Sudoku

curl -X POST http://localhost:8080/api/v1/problems/sudoku \
  -H "Content-Type: application/json" \
  -d '{
    "grid": [
      [5,3,0,0,7,0,0,0,0],
      [6,0,0,1,9,5,0,0,0],
      [0,9,8,0,0,0,0,6,0],
      [8,0,0,0,6,0,0,0,3],
      [4,0,0,8,0,3,0,0,1],
      [7,0,0,0,2,0,0,0,6],
      [0,6,0,0,0,0,2,8,0],
      [0,0,0,4,1,9,0,0,5],
      [0,0,0,0,8,0,0,7,9]
    ]
  }'

Solve Graph Coloring

Nodes are named; edges are pairs of node indices. Returns UNSATISFIABLE when the graph is not k-colorable (for example a triangle with two colors).

curl -X POST http://localhost:8080/api/v1/problems/graph-coloring \
  -H "Content-Type: application/json" \
  -d '{
    "nodes": ["A", "B", "C"],
    "edges": [[0, 1], [1, 2], [2, 0]],
    "numColors": 3
  }'

Algorithms

Backtracking Search

The core solver uses depth-first backtracking search with:

• Trailing rollback: each search node snapshots only the domains it mutates and restores exactly those on backtrack, instead of copying the whole domain map per node. Domains are BitSet-backed with a cheap checkpoint/rollback.
• Constraint propagation: forward checking removes inconsistent values from future domains after each assignment and detects domain wipeouts early.
• Heuristic ordering: variable selection narrows the search tree; the search is complete (it can prove unsatisfiability and enumerate multiple solutions).

Variable Ordering Heuristics

Heuristic	Description
MRV	Minimum Remaining Values - choose variable with smallest domain
Degree	Choose variable involved in most constraints
Dom/WDeg	Domain size divided by weighted degree (learned from failures)
MRV+Degree	MRV with Degree as tiebreaker (default)

AC-3 Arc Consistency

Before search begins, AC-3 enforces arc consistency:

1. For each arc (Xi, Xj), remove values from Xi that have no support in Xj
2. Propagate changes to affected arcs
3. Repeat until no changes or domain wipeout

Min-Conflicts (for large N-Queens)

The N-Queens endpoint switches to min-conflicts local search for N >= 50:

1. Initialize with a greedy assignment
2. Pick a conflicted variable
3. Move to value with minimum conflicts
4. Repeat until solution or max iterations

This path is fast but incomplete: it cannot prove unsatisfiability or return all solutions.

Built-in Problems

Exposed over REST:

N-Queens

Place N queens on an NxN chessboard so no two queens attack each other.

Sudoku

Fill a 9x9 grid so each row, column, and 3x3 box contains digits 1-9.

Graph Coloring

Color nodes of a graph with k colors so no adjacent nodes share a color.

Cryptarithmetic

Assign distinct digits to letters so an equation like SEND + MORE = MONEY holds. Leading letters are restricted to 1-9, and the solver verifies every complete assignment against all constraints, so SEND+MORE=MONEY returns exactly its unique solution (9567 + 1085 = 10652).

WebSocket

Live search progress is streamed over STOMP. Publish a solve command to /app/solve with a sessionId, then subscribe to /topic/solver/{sessionId} to receive per-step events (variable selection, value assignment, backtracks, solutions, completion). N-Queens is used as the streamed problem because its systematic search produces a rich event stream.

The solver also publishes throttled PROGRESS events (at most ~30 per second) carrying the current partial assignment as a {variable: value} map plus node and backtrack counts, so a client can render live board state without replaying every per-node event. A ready-made client ships with the app: run it and open http://localhost:8080/visualize.html for a live chessboard visualization of the search.

const socket = new SockJS('/ws/solver');
const stompClient = Stomp.over(socket);

stompClient.connect({}, () => {
  const sessionId = 'demo-1';
  stompClient.subscribe('/topic/solver/' + sessionId, (message) => {
    console.log('Progress:', JSON.parse(message.body));
  });
  stompClient.send('/app/solve', {}, JSON.stringify({ sessionId, n: 12 }));
});

Configuration

Application configuration in application.yml:

server:
  port: 8080

solver:
  default-timeout-ms: 60000
  max-solutions: 1000

springdoc:
  swagger-ui:
    path: /swagger-ui.html

Project Structure

src/main/java/com/cspsolver/
├── core/
│   ├── model/          # CSP, Variable, Domain, Assignment
│   ├── constraint/     # Constraint interfaces and implementations
│   └── propagation/    # AC-3, Forward Checking
├── solver/
│   ├── backtracking/   # BacktrackingSolver
│   └── heuristics/     # MRV, Degree, LCV selectors
├── problems/           # Built-in problem factories
├── api/
│   ├── controller/     # REST controllers
│   └── dto/            # Request/Response DTOs
└── websocket/          # WebSocket configuration

Development

Run Tests

mvn test

Build JAR

mvn clean package
java -jar target/csp-solver-1.0.0-SNAPSHOT.jar

Code Coverage

mvn verify
# Reports in target/site/jacoco/

Docker

Build Image

docker build -t csp-solver .

Run Container

docker run -p 8080:8080 csp-solver

Docker Compose

docker-compose up -d

API Health Check

curl http://localhost:8080/actuator/health

License

MIT License. See LICENSE for the full text.