Solving Constraint Satisfaction Problems via Propositional Satisfiability (SAT)

1. Problem Formulation

Given an $m \times n$ matrix $G$ containing blank cells and cells with non-negative integers $k$ (where $0 \le k \le 9$), the goal is to assign a binary color state (Green or Red) to every cell $C_{i,j}$.

. 2 3 . . 0 . . . .
. . . . 3 . 2 . . 6
. . 5 . 5 3 . 5 7 4
. 4 . 5 . 5 . 6 . 3
. . 4 . 5 . 6 . . 3
. . . 2 . 5 . . . .
4 . 1 . . . 1 1 . .
4 . 1 . . . 1 . 4 .
. . . . 6 . . . . 4
. 4 4 . . . . 4 . .

The core constraint states: For every cell $C_{i,j}$ containing an integer $k$, exactly $k$ cells within its Moore neighborhood (the 3x3 grid centered on $C_{i,j}$, including itself) must be colored Green.

Let $x_{i,j}$ be a boolean propositional variable where:

• $x_{i,j} = \text{True}$ signifies the cell is Green.
• $x_{i,j} = \text{False}$ signifies the cell is Red.

For a neighborhood $N(i,j)$ surrounding a constrained cell, the mathematical requirement is a cardinality constraint: $\sum_{v \in N(i,j)} v = k$

2. Logical Encoding & Methodology

Directly solving cardinality constraints is not natively supported by standard SAT solvers, which only accept propositional formulas in Conjunctive Normal Form (CNF). The primary academic challenge of this project was encoding the "exactly $k$" constraint efficiently.

2.1. Variable Pool Management

A propositional variable mapper (pysat.formula.IDPool) was utilized to create a bijection between the 2D spatial coordinates $(i, j)$ and a 1D sequence of integer literals required by the SAT solver.

2.2. Optimized Cardinality Encoding (Sequential Counters)

A naive approach to encoding an "exactly $k$" constraint involves generating combinations of literals, which leads to a combinatorial explosion of clauses—specifically $O(2^{|N|})$ clauses, severely degrading solver performance as the grid scales.

To achieve polynomial time complexity during the CNF translation, this implementation utilizes Sequential Counter Encoding (EncType.seqcounter).

• Instead of pure combinations, the algorithm introduces auxiliary variables that act as intermediate states in a digital adder circuit.
• This encoding translates the cardinality constraint into a set of CNF clauses that scale linearly $O(|N| \cdot k)$, drastically reducing the memory footprint and the depth of the search tree.

3. Solver Integration & Execution

The generated CNF clauses are fed into the Glucose3 solver. Glucose3 is heavily optimized for solving deeply constrained industrial problems. By leveraging unit propagation and clause learning, the solver avoids exploring dead-end branches in the state space.

• Satisfiability: If a valid configuration exists, the solver returns a model (a list of boolean assignments), which is then reverse-mapped back to the $m \times n$ grid to render the final colored matrix.
• Unsatisfiability: If the provided initial matrix contains logical contradictions, the solver mathematically proves that no solution exists.

4. Conclusion & Applications

This project successfully demonstrates the power of reducing complex domain-specific rules into pure propositional logic. By optimizing the CNF encoding process via Sequential Counters, the system transforms a visually complex puzzle into a highly optimized, machine-solvable format.

The methodologies explored here—specifically cardinality encoding and boolean reduction—are directly applicable to large-scale scheduling, resource allocation, and automated theorem proving.

Further Reading & Source Code

For a deep dive into the methodology, detailed evaluation metrics, and the full implementation, please visit the repository: https://github.com/LPH1110/tdtu_ai_final_N14/tree/main/source/task3.