Exact-Cover-SAT

Encodes, solves, and decodes the exact cover problem via reduction to SAT.

Documentation

Problem description

"Given a collection $S$ of subsets of a set $X$ , an exact cover is a subcollection $S^{*}$ of $S$ such that each element in $X$ is contained in exactly one subset in $S^*$ . It is a non-deterministic polynomial time $(NP)$ complete problem and has a variety of applications, ranging from the optimization of airline flight schedules, cloud computing, and electronic circuit design." Source.

Example of a valid input file format:

{1 2 3 4}
{
    { }
    {1 3}
    {1 2 3}
    {2 4}
}

Input format:

• First line only contains the main set: $X$.
• Following lines only contain the set of subsets of the main set: $S$.
• Both subsets of literals and the set of subsets $S$ need to be contained in { }.
• Lines after the main set can contain multiple subsets.
• Literals need to be delimited by (one or more) spaces.
• Literals can be strings of various length but without whitespace.

This input file format is also valid:

{alpha bravo charlie delta}
{ { } {alpha charlie} {alpha bravo charlie} {bravo delta} }

Any deviation from the problem's specifications (e.g., subset contains an element that is not present in the main set) should trigger an exception during parsing.

Encoding

The problem is encoded using one set of variables. Variable $s_i$ represents that subset $S_i$ is included in the exact cover $S^{*}$.
Analogically, variable $\neg s_i$ means the subset is not included in $S^*$.

The conditions for a collection of subsets to be an exact cover of the main set $X$ can be written as the following constraints:

• Every element of the main set $X$ has to be included in at least one subset in $S^*$.

$$\bigwedge_{e \in X} \left( \bigvee_{\substack{ S_i \in S \\ e \in S_i}} (s_i) \right)$$

• Every element of the main set $X$ can be included in at most one subset in $S^*$.

$$\bigwedge_{e \in X} \left( \bigwedge_{\substack{S_i, S_j \in S\\ S_i \neq S_j}} \left(\neg s_i \lor \neg s_j \right) \right)$$

User documentation

Basic usage:

main.py [-h] [-i INPUT] [-o OUTPUT] [-s SOLVER] [-v {0,1}]

Command-line options:

• -h, --help : Show a help message and exit.
• -i INPUT, --input INPUT : The instance file. Default: "input.in".
• -o OUTPUT, --output OUTPUT : Output file for the DIMACS cnf formula. Default: "output.cnf".
• -s SOLVER, --solver SOLVER : The SAT solver to be used. Default "glucose-syrup" *
• -v {0,1}, --verb {0,1} : Verbosity of the SAT solver used.

* If the provided path cannot be found, the script assumes this to be a global command.

Example instances

• input-easy-sat.in: Simple satisfiable instance provided in the Exact cover wikipedia page where $|X| = 4$, $|S| = 4$.
• input-easy-unsat.in: Simple unsatisfiable instance where $|X| = 5$, $|S| = 5$.
• input-hard-sat.in: Complex satisfiable instance generated using instance_generator.py where $|X| = 100$, $|S| = 560$.
• input-hard-unsat.in: Complex unsatisfiable instance generated using instance_generator.py where $|X| = 100$, $|S| = 500$.

Experiments

Experiments were run on Intel Core i7-7500U CPU (2.70GHz) and 12 GB RAM on Fedora Linux 40.

The following values are averages over 5 runs of glucose-syrup on various instances generated by the instance_generator.py with the given parameters and GUARANTEED_SAT set to True.

For SUBSET_COUNT_MULT set to 5:

Main set size	Variable count	Clause count	Runtime (s)
20	113	25360	0.123
40	226	196185	1.358
60	338	707458	6.892
80	451	1586590	20.177
100	561	3081377	46.554

---

For SUBSET_COUNT_MULT set to 10:

Main set size	Variable count	Clause count	Runtime (s)
20	214	105004	0.763
40	425	831246	10.331
60	641	2813321	49.826
80	849	6402951	12.339
100	1064	12434209	24.045

---

SUBSET_COUNT_MULT specifies how many random subsets of $X$ will be created. For example if MAIN_SET_SIZE = 20 and SUBSET_COUNT_MULT = 5, then $100$ random subsets will be created.