SAT Encoding for Set of At-Most-K Cardinality Constraints with Ladder Shape

Hieu Truong Xuan; Tuyen Kieu Van; Khanh To Van

cs.AINov 3, 2026

SAT Encoding for Set of At-Most-K Cardinality Constraints with Ladder Shape

Authors: Hieu Truong Xuan, Tuyen Kieu Van, Khanh To Van

Organizations: University of Engineering and Technology, Vietnam National University, Hanoi, Vietnam.

Abstract

This paper presents a novel SAT encoding designed to represent a sequence of At-Most-K cardinality constraints arranged in a ladder-like structure, referred to as the Ladder AMK constraint. These AMK constraints feature a ladder-like arrangement, with shared common variables in the center and two variables differing at the beginning and the end. The proposed encoding first decomposes the sequence of AMK constraints into separated blocks, then encodes each block as a whole rather than encoding each AMK constraint individually. This approach improves the efficiency of constraint solving in SAT solvers by significantly reducing the size of the encoding, precisely the number of variables, and the generated clauses required. To achieve this, the encoding employs Sequential Counter to encode each block and constructs clauses that link adjacent blocks, ensuring equivalence with the input constraints. Compared to the previously proposed encoding that uses BDD for Ladder AMO constraint, our encoding requires fewer variables and clauses. Our study is the first study that develops SAT encoding for Ladder AMK constraints with k>1. Experimental results on single Ladder AMO and Ladder AMK constraints indicate that our encoding significantly enhances both the size of the encoding and the efficiency of solving time compared to existing encodings. Furthermore, by evaluating on the two real-world combinatorial problems, namely Anti-bandwidth Problem and Nurse Rostering Problem, we found that the proposed encoding surpasses alternative encodings, as well as more advanced Constraint Programming and Mixed Integer Programming solvers. In summary, the SAT encoding technique presented in this paper provides a more efficient method for encoding sequence constraint, specifically Ladder AMK constraint, which could enhance the effectiveness of SAT solving for various problems involving this type of constraint.

Figures & tables

x_{1}

x_{2}

x_{3}

x_{4}

\leq k\wedge

x_{2}

x_{3}

x_{4}

x_{5}

\leq k\wedge

x_{3}

x_{4}

x_{5}

x_{6}

\leq k\wedge

x_{4}

x_{5}

x_{6}

x_{7}

\leq k\wedge

x_{5}

x_{6}

x_{7}

x_{8}

\leq k\wedge

x_{6}

x_{7}

x_{8}

x_{9}

\leq k\wedge

Figure 1: Ladder AMK constraint of 10 variables and width 4.

c_{1,o}

c_{2,o}

c_{3,o}

c_{4,o}

c_{5,o}

\leq 2\wedge

c_{2,o}

c_{3,o}

c_{4,o}

c_{5,o}

c_{6,o}

\leq 2\wedge

c_{3,o}

c_{4,o}

c_{5,o}

c_{6,o}

c_{7,o}

\leq 2\wedge

c_{4,o}

c_{5,o}

c_{6,o}

c_{7,o}

c_{8,o}

\leq 2\wedge

c_{5,o}

c_{6,o}

c_{7,o}

c_{8,o}

c_{9,o}

\leq 2\wedge

c_{6,o}

c_{7,o}

c_{8,o}

c_{9,o}

c_{10,o}

\leq 2

Figure 2: Ladder AMK constraint ensuring that for any 5 consecutive cars in a sequence of 10 cars, at most 2 cars can be equipped with option

o

x_{i,1,N}

x_{i,2,N}

\ldots

x_{i,14,N}

\leq 8\wedge

x_{i,2,N}

\ldots

x_{i,14,N}

x_{i,15,N}

\leq 8\wedge

\ldots

\leq 8\wedge

x_{i,14,N}

x_{i,15,N}

\ldots

x_{i,27,N}

\leq 8\wedge

x_{i,15,N}

\ldots

x_{i,27,N}

x_{i,28,N}

\leq 8

Figure 3: Ladder AMK constraint ensuring that nurse

i

works at most 8 night shifts in any 14 consecutive days over a 28-day planning horizon.

$\mathcal{E}_{1}$	=	$v_{1}$
$\mathcal{E}_{2}$	=	$v_{1}$	+	$v_{2}$
$\ldots$	=	$\ldots$
$\mathcal{E}_{w}$	=	$v_{1}$	+	$v_{2}$	+	$\ldots$	+	$v_{w}$

Figure 4: A block consisting of a sequence of

w

variables

\{v_{1},\ldots,v_{w}\}

x_{1}

x_{2}

x_{3}

x_{4}

\leq k

x_{2}

x_{3}

x_{4}

x_{5}

A_{2}

\leq k

x_{3}

x_{4}

x_{5}

x_{6}

\leq k

A_{1}

x_{4}

x_{5}

x_{6}

x_{7}

\leq k

x_{5}

x_{6}

x_{7}

x_{8}

\leq k

x_{5}

x_{6}

x_{7}

x_{8}

A_{4}

\leq k

Figure 5: Decomposition of an Ladder AMK constraint with

n=10

and

w=4

$x_{2}$	+	$x_{3}$	+	$x_{4}$
$x_{2}$	+	$x_{3}$	+	$x_{4}$	$\equiv$	$R_{1,3,1},R_{1,3,2}$
		$x_{3}$	+	$x_{4}$	$\equiv$	$R_{1,2,1},R_{1,2,2}$
				$x_{4}$	$\equiv$	$R_{1,1,1}$

Figure 6: Register bit construction of block

A_{1}

under the condition

\leq 2

x_{1}

x_{2}

x_{3}

x_{4}

\leq 2

x_{2}

x_{3}

x_{4}

x_{5}

A_{2}

\leq 2

x_{3}

x_{4}

x_{5}

x_{6}

\leq 2

A_{1}

x_{4}

x_{5}

x_{6}

x_{7}

\leq 2

x_{5}

x_{6}

x_{7}

x_{8}

\leq 2

x_{5}

x_{6}

x_{7}

x_{8}

A_{4}

\leq 2

Figure 7: Decomposition of Ladder At-Most-Two constraint.

$A_{1}$
$x_{1}$	+	$x_{2}$	+	$x_{3}$	+	$x_{4}$
		$x_{2}$	+	$x_{3}$	+	$x_{4}$	$\equiv$	$R_{1,3,1},R_{1,3,2}$
				$x_{3}$	+	$x_{4}$	$\equiv$	$R_{1,2,1},R_{1,2,2}$
						$x_{4}$	$\equiv$	$R_{1,1,1}$
$A_{2}$
$x_{5}$							$\equiv$	$R_{2,1,1}$

Figure 8: Register bits constructing of Ladder At-Most-Two constraint.

Encoding	Technique	Auxiliary variables	Clauses	Complexity
Pairwise	Encode each AMK constraint separately	0	$C^{w}_{k+1}+(N-1)C^{w-1}_{k}$	$\mathcal{O}(n^{k+1})$
Seq		$Nk(w-2)$	$N(3kw-7k+w)$	$\mathcal{O}(n^{2}k)$
BDD		$N(w-k)(k+1)$	$2N(w-k)(k+1)$	$\mathcal{O}(n^{2}k)$
Card		$\mathcal{O}(n^{2}\text{log}_{2}^{2}k)$	$\mathcal{O}(n^{2}\text{log}_{2}^{2}k)$	$\mathcal{O}(n^{2}\text{log}_{2}^{2}k)$
Adder		$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$
$SCL_{\leq k}$	Encode set of AMK constraints	$(2M-2)(wk-\frac{k^{2}+k}{2}-1)$	$9Mkw-5Mk^{2}-Mw-7Mk-9kw$	$\mathcal{O}(nk)$

Table 1: Size of SAT encoding for a Ladder AMK constraint over

n

variables with width

w

N=(n-w)+1

and

M=\left\lceil\frac{n}{w}\right\rceil

Figure 9: Forward and backward BDDs for Ladder AMO constraint.

Encoding	Technique	Auxiliary variables	Clauses	Complexity
Pairwise	Encode each AMO constraint separately	0	$\frac{(w-1)w}{2}+(N-1)(w-1)$	$\mathcal{O}(n^{2})$
Seq		$N(w-2)$	$N(4w-7)$	$\mathcal{O}(n^{2})$
BDD		$2N(w-1)$	$4N(w-1)$	$\mathcal{O}(n^{2})$
Card		$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$
Adder		$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$	$\mathcal{O}(n^{2})$
Product		$N(2\sqrt{w}+\mathcal{O}\sqrt[4]{w})$	$N(2w+4\sqrt{w}+\mathcal{O}\sqrt[4]{w})$	$\mathcal{O}(n^{2})$

Table 2: Size of SAT encoding for a Ladder AMO constraint over

n

variables with width

w

N=(n-w)+1

and

M=\left\lceil\frac{n}{w}\right\rceil

x_{i}^{1}

+

x_{i}^{2}

+

x_{i}^{3}

+

x_{i}^{4}

+

x_{i^{\prime}}^{1}

+

x_{i^{\prime}}^{2}

+

x_{i^{\prime}}^{3}

+

x_{i^{\prime}}^{4}

\leq 1

x_{i}^{2}

+

x_{i}^{3}

+

x_{i}^{4}

+

x_{i}^{5}

+

x_{i^{\prime}}^{2}

+

x_{i^{\prime}}^{3}

+

x_{i^{\prime}}^{4}

+

x_{i^{\prime}}^{5}

\leq 1

x_{i}^{3}

+

x_{i}^{4}

+

x_{i}^{5}

+

x_{i}^{6}

+

x_{i^{\prime}}^{3}

+

x_{i^{\prime}}^{4}

+

x_{i^{\prime}}^{5}

+

x_{i^{\prime}}^{6}

\leq 1

x_{i}^{4}

+

x_{i}^{5}

+

x_{i}^{6}

+

x_{i}^{7}

+

x_{i^{\prime}}^{4}

+

x_{i^{\prime}}^{5}

+

x_{i^{\prime}}^{6}

+

x_{i^{\prime}}^{7}

\leq 1

x_{i}^{5}

+

x_{i}^{6}

+

x_{i}^{7}

+

x_{i}^{8}

+

x_{i^{\prime}}^{5}

+

x_{i^{\prime}}^{6}

+

x_{i^{\prime}}^{7}

+

x_{i^{\prime}}^{8}

\leq 1

x_{i}^{6}

+

x_{i}^{7}

+

x_{i}^{8}

+

x_{i}^{9}

+

x_{i^{\prime}}^{6}

+

x_{i^{\prime}}^{7}

+

x_{i^{\prime}}^{8}

+

x_{i^{\prime}}^{9}

\leq 1

x_{i}^{7}

+

x_{i}^{8}

+

x_{i}^{9}

+

x_{i}^{10}

+

x_{i^{\prime}}^{7}

+

x_{i^{\prime}}^{8}

+

x_{i^{\prime}}^{9}

+

x_{i^{\prime}}^{10}

\leq 1

Figure 12: OBJ-k constraint of {

i

i^{\prime}

} with

|V|=10

and

k=3

Table 14

Small instances					Large instances
Instance	$\|$ V $\|$	$\|$ E $\|$	LB	UB	Instance	$\|$ V $\|$	$\|$ E $\|$	LB	UB
A-pores_1	30	103	6	8	M-bcsstk06	420	3720	28	72
B-ibm32	32	90	9	9	N-bcsstk07	420	3720	28	72
C-bcspwr01	39	46	16	17	O-impcol_d	425	1267	91	173
D-bcsstk01	48	176	8	9	P-can__445	445	1682	78	120
E-bcspwr02	49	59	21	22	Q-494_bus	494	586	219	246

Table 5: Harwell-Boeing Sparse Matrix benchmark.

Instance	LB	UB	Duplex			$SCL_{seq}$			$SCL_{par}$			CPLEX			CP-SAT
Instance	LB	UB	Obj-k	Time(s)	MB	Obj-k	Time(s)	MB	Obj-k	Time(s)	MB	Obj-k	Time(s)	MB	Obj-k	Time(s)	MB
M-bcsstk06	28	72	35	TO	1726	35	TO	1398	35	TO	5076	30	TO	738.4	33	TO	5243
N-bcsstk07	28	72	35	TO	1726	35	TO	1397	35	TO	5291	30	TO	737.9	33	TO	5250
O-impcol_d	91	173	101	TO	1745	102	TO	1802	106	TO	5366	121	TO	491.3	93	TO	5388
P-can__445	78	120	-	TO	2464	79	TO	2156	81	TO	9758	79	TO	869.2	-	TO	5732
Q-494_bus	219	246	-	TO	1443	220	TO	1301	220	TO	4713	220	TO	701.6	-	316.8	MO

Table 6: ABP solving results of the five best approaches in 12 large instances with TO = 1800s and MO = 30GB.

Work period	40 days		60 days		80 days		100 days
Work period	Time(ms)	MB	Time(ms)	MB	Time(ms)	MB	Time(ms)	MB
Adder	192	9.6	302	15	419	19.3	535	26.4
BDD	49	8.9	94	15.2	145	23	187	28
Card	107	10.8	143	16.7	180	24.5	212	29.5
Pairwise	-	MO	-	MO	-	MO	-	MO
SCL	16	5.7	25	8.6	33	11.5	42	13.4

Table 7: NRP solving results of different approaches with TO = 600s and MO = 5GB.

Boolean Satisfiability

See all 25 papers

Jul 23, 2026

Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning

The Single Constant Multiplication problem is a fundamental NP-hard optimization task in hardware design, which seeks to decompose a fixed constant using only additions, subtractions, and bit-shifts. Although dynamic programming methods can produce near-optimal SAT encodings for SCM, their encoding cost remains high for large constants. We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition. Our approach employs a graph neural network model to predict promising operator types from constant decompositions, and exploits the resulting confidence scores to prune no-good choices in the symbolic search. Experimental results on unseen 17-32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97% reduction in memory usage, and an order-of-magnitude decrease in branching, while preserving near-optimal encoding quality in terms of additions. These results show that learning-guided symbolic strategies can significantly improve the scalability and efficiency of SCM encoding. Our code and data are publicly available at: https://github.com/Chufeng-Jiang/SCM_MLDP

Chufeng Jiang, Neng-Fa Zhou

Graduate Center, The City University of New York · The City University of New York New York, USA

Electronic Design Automation

Ask PDF

Mar 19, 2026

When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)

Classical planning problems are typically defined using lifted first-order representations, which offer compactness and generality. While most planners ground these representations to simplify reasoning, this can cause an exponential blowup in size. Recent approaches instead operate directly on the lifted level to avoid full grounding. We explore a middle ground between fully lifted and fully grounded planning by introducing three SAT encodings that keep actions lifted while partially grounding predicates. Unlike previous SAT encodings, which scale quadratically with plan length, our approach scales linearly, enabling better performance on longer plans. Empirically, our best encoding outperforms the state of the art in length-optimal planning on hard-to-ground domains.

João Filipe, Gregor Behnke

University of Amsterdam, Institute for Logic Language and Computation, The Netherlands

Classical Planning Symbolic Planning

Ask PDF

Apr 16, 2026

Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

Foundational optimization embeddings have recently emerged as powerful pre-trained representations for mixed-integer programming (MIP) problems. These embeddings were shown to enable cross-domain transfer and reduce reliance on solver-generated labels. In this work, we investigate whether such representations generalize beyond optimization to decision problems, focusing on Boolean satisfiability (SAT). We adapt the foundational optimization architecture to SAT by mapping CNF formulas into the same bipartite constraint-variable graph representation used for MIPs. This allows direct reuse of the pre-trained embedding model without architectural changes or supervised fine-tuning. Our results show that these embeddings capture structural regularities in SAT instances and support unsupervised tasks such as instance clustering and distribution identification. We demonstrate, for the first time, that foundational optimization embeddings can transfer to constraint satisfaction domains. Our findings is a step toward a unified representational framework for both optimization and decision problems.

Koyena Pal, Serdar Kadioglu

AI Center of Excellence, Fidelity Investments, USA · Khoury College of Computer Sciences, Northeastern University, USA · Department of Computer Science, Brown University, USA

Unsupervised Representation Learning Transfer Learning Constraint Satisfaction Boolean Satisfiability

Ask PDF

Abstract

Boolean Satisfiability

Explore similar work

Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning

When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)

Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations