Sharing the Count: A Smaller SAT Encoding for Sliding-Window Rules

Rules such as “no more than four night shifts in any fourteen days” repeat almost the same calculation as the calendar advances. Researchers at Vietnam National University, Hanoi, propose exploiting that overlap rather than asking a SAT solver to handle each window separately.

When neighboring rules repeat themselves

Many scheduling rules concern a moving window: inspect several consecutive days, count a particular activity, and enforce a limit. Move forward one day, and almost everything being counted stays the same.

Hieu Truong Xuan, Tuyen Kieu Van and Khanh To Van study how to exploit this repetition when translating a problem into Boolean satisfiability, or SAT. A SAT solver searches for true-or-false assignments that satisfy a collection of logical clauses. The translation matters because different formulas can express the same requirements while demanding different amounts of memory and solving time.

The paper focuses on “Ladder At-Most-K” constraints. Each window contains the same number of Boolean variables, at most k of which may be true. Neighboring windows share every variable except the one leaving and the one entering. Written underneath one another, these overlapping rules form a ladder-like pattern.

For example, a production sequence might allow at most two cars with a particular option among any five consecutive cars. Treating every five-car window independently repeats much of the counting work.

Count blocks, then connect them

The proposed method, Sequential Counter encoding for Ladder constraints, or SCL, divides the original sequence into groups of variables. It constructs counting blocks over those groups, using forward and backward orders where needed to represent the portions of windows crossing group boundaries.

Inside each block, auxiliary Boolean variables record counting thresholds: whether the first few variables contain at least one true value, at least two, and so on up to k. These intermediate results can serve several overlapping windows instead of being rebuilt for each one.

Connecting clauses then prevent neighboring blocks from jointly exceeding the limit. If one side of a window already contains k true variables, the other side must contain none. If it contains k minus one, the other side can contribute at most one. The encoding expresses these combinations through the shared threshold variables.

The authors add clauses that establish when those threshold variables must be false as well as true. This gives the reused counts the meaning needed for the connections. The paper includes a soundness and completeness proof for its individual-block encoding.

Its size analysis gives SCL an O(nk) bound, where n is the sequence length. That is linear in n when k is fixed. By comparison, separately encoding each window with a sequential counter has an O(n²k) worst-case bound when the window width is approximately half the sequence length. For the at-most-one case, SCL and the earlier Duplex method both have linear bounds, but SCL uses fewer auxiliary variables and clauses in the paper’s comparison.

Faster in most standalone tests

The experiments used the CaDiCaL SAT solver. For standalone constraints allowing more than one true variable per window, SCL was fastest in three of four tested window-and-limit configurations. A direct encoding that forbids every combination of k plus one true variables won the smallest configuration: windows of ten with a limit of two.

At 5,000 variables, with windows of 100 and a limit of 20, SCL took 46.6 milliseconds, compared with 298.4 milliseconds for the binary decision diagram encoding. The direct combination-based encoding exceeded the 600-second limit throughout the tested input sizes for that configuration and for windows of 50 with a limit of ten.

Scheduling and graph-labeling results

The scheduling benchmark constructed a roster for one nurse over 40, 60, 80 or 100 days, subject to eleven requirements. These included limits on night and evening shifts, minimum rest periods and restrictions on consecutive nights. Minimum-count rules were converted into equivalent maximum-count rules where needed.

Across ten runs per instance, SCL had the lowest reported average solving time and memory use among the compared approaches. For 100 days, it took 42 milliseconds and 13.4 MB, versus 106 milliseconds and 47.4 MB for the ordinary sequential-counter approach. Gurobi took 59 milliseconds and 16.4 MB.

The graph benchmark addressed anti-bandwidth: assigning distinct numeric labels to vertices while maximizing the smallest label difference across an edge. The authors tested 24 graphs and introduced an SCL search using up to four parallel SAT processes.

Parallel SCL obtained better reported feasible values than Duplex on five of the twelve large graphs. It was not uniformly best: CPLEX obtained a better value on one large graph and solved some others faster. Many large-instance runs reached the time limit, so their reported feasible values are not all proven optima.

The central contribution is a representation strategy: reuse the counts hidden inside overlapping rules. The experiments show how that strategy can reduce formula size and improve solving performance without changing the requirements being enforced.