🧩 Constraint Solving POTD:Problem of the Day: Vertex Cover via SAT Encoding

[github-actions[bot]]

Problem Statement

The vertex cover problem asks: given an undirected graph with vertices and edges, find a minimum-size subset of vertices such that every edge has at least one endpoint in the subset.

Concrete Instance:
Consider a 5-vertex graph:

Vertices: {1, 2, 3, 4, 5}
Edges: {(1,2), (2,3), (3,4), (4,5), (5,1), (1,3)}

A valid vertex cover might be {1, 3, 4} (size 3), where each edge touches at least one chosen vertex. The goal is to find the smallest such set.

Input/Output:

• Input: Graph G = (V, E) and (optionally) a budget k
• Output: A set S ⊆ V where for every (u, v) ∈ E, either u ∈ S or v ∈ S, minimizing |S|

Why It Matters

Network security: Detecting compromised devices in a communication network—cover vertices (secured nodes) to monitor all connections. Protein interaction networks: Identifying key proteins that interact with many others to reduce experimental validation costs. Code coverage: Selecting minimal test cases to exercise all code paths (edges = dependencies, vertices = tests).

Modeling Approaches

Approach 1: Direct SAT Encoding (Decision Variant)

For a fixed budget k, encode the decision problem into CNF:

Decision Variables:
x_i ∈ {0, 1} for each vertex i, where x_i = 1 means vertex i is in the cover.

Constraints:

1. Edge coverage (CNF clauses): For each edge (u, v), require x_u ∨ x_v (at least one endpoint selected)
2. Budget constraint: ∑ x_i = k (or ≤ k)—encoded as a cardinality constraint in CNF

Trade-offs:

• Strength: Direct encoding; modern SAT solvers (CDCL) excel on sparse instances
• Weakness: Solving multiple k values requires re-encoding; cardinality encoding can blow up in size

Example SAT Model (CNF)

c Vertex cover for 5 vertices, 6 edges, budget k=3
c Variables: x1, x2, x3, x4, x5
p cnf 5 10

c Edge coverage clauses
1 2 0        c (1,2): x1 ∨ x2
2 3 0        c (2,3): x2 ∨ x3
3 4 0        c (3,4): x3 ∨ x4
4 5 0        c (4,5): x4 ∨ x5
5 1 0        c (5,1): x5 ∨ x1
1 3 0        c (1,3): x1 ∨ x3

c Cardinality: at most 3 vertices
c (simplified: totalizer encoding adds auxiliary vars)
-1 -2 -3 -4 -5 0

Approach 2: Integer Linear Programming (ILP)

Model vertex cover as an optimization problem:

Variables:
x_i ∈ {0, 1} for each vertex i

Objective:
Minimize ∑_{i=1}^{|V|} x_i

Constraints:
For each edge (u, v): x_u + x_v ≥ 1

Trade-offs:

• Strength: Continuous relaxation provides lower bounds; branch-and-bound naturally optimizes over all k
• Weakness: LP relaxation is loose; requires strong branching strategies

Approach 3: Hybrid SAT + Incremental Search

Interleave SAT solving with an outer loop on k:

1. Start with k = |E| (trivial upper bound: any edge endpoint set)
2. Call SAT solver with k (encoded with unit propagation shortcuts)
3. If satisfiable, decrement k and retry
4. If unsatisfiable, the previous k is optimal

Trade-offs:

• Strength: Leverages SAT solver strengths; reuses learned clauses across iterations
• Weakness: May solve many instances; but each problem is often easier than random SAT

Key Techniques

1. CNF Encoding of Constraints

The edge-coverage constraint x_u ∨ x_v is already in CNF—one clause per edge. Cardinality constraints like ∑ x_i ≤ k require auxiliary variables (Tseitin transformation) or specialized encodings (totalizer, sorter networks).

2. Symmetry & Lower Bounds

Vertex degree can guide heuristics: high-degree vertices are "more likely" in a minimal cover. Greedy lower bounds (e.g., maximal matching gives a lower bound of |matching|) help prune the search space.

3. SAT Solver Internals

Modern solvers employ:

• Unit propagation: x_u ∨ x_v with x_u = 0 forces x_v = 1
• Conflict-driven clause learning (CDCL): Analyzes conflicts to add learned clauses that avoid similar conflicts
• Restarts & branching heuristics: Variable selection strategies (VSIDS, LRB) prioritize frequently-conflicting variables

Challenge Corner

Can you encode the optimization problem directly in SAT without an outer loop?

One approach: use a SAT-based optimization framework (like SAT-IP hybrids or core-guided MaxSAT). Alternatively, think about how a SAT solver could learn that no vertex cover of size < k exists, automatically finding the minimum.

Advanced: How would you handle weighted vertex cover (minimize ∑ w_i x_i) using SAT? Is incremental weakening of cardinality constraints practical?

References

1. Arora & Barak (2009). Computational Complexity: A Modern Approach, Ch. 2.1—NP-completeness of vertex cover and SAT encodings.
2. Biere, Heule, van Maaren & Walsh (eds., 2009). Handbook of Satisfiability, Ch. 2 & 4—CNF encodings, SAT solver algorithms, and cardinality constraints.
3. Eén & Sörensson (2006). "Translating Pseudo-Boolean Constraints into SAT"—practical cardinality encoding techniques.
4. Xiao & Gao (2018). Handbook of Approximation Algorithms and Metaheuristics — vertex cover approximation and exact algorithms via IP/SAT.

Generated by 🧩 Constraint Solving — Problem of the Day · copilot · haiku45 · 8.13 AIC · ⌖ 6.68 AIC · ⊞ 6.1K · ◷

• expires on Oct 13, 2026, 3:35 AM UTC-08:00

[github-actions[bot]]

This discussion has been marked as outdated by Constraint Solving — Problem of the Day.

A newer discussion is available at Discussion #66531.