Experimental results

Many of the ideas that we have described have been implemented in the PBCHAFF satisfiability solver. In an earlier paper [Dixon GinsbergDixon Ginsberg2002], we compared results obtained using PRS, a pseudo-Boolean version of RELSAT, and those obtained using RELSAT [Bayardo MirankerBayardo Miranker1996]. PBCHAFF is an updated version of PRS that is modeled closely on ZCHAFF [Moskewicz, Madigan, Zhao, Zhang, MalikMoskewicz et al.2001]. It implements watched literals for cardinality constraints and applies the strengthening idea. Here we compare PBCHAFF's performance to its Boolean counterpart ZCHAFF.

Table 1: Run time (seconds) and nodes expanded

	ZCHAFF		PBCHAFF
Instance	sec	nodes	sec	nodes
2pipe	0	8994	0	8948
2pipe-1-ooo	1	10725	1	9534
2pipe-2-ooo	0	6690	0	6706
3pipe	7	48433	12	57218
3pipe-1-ooo	6	33570	9	36589
3pipe-2-ooo	9	41251	16	45003
3pipe-3-ooo	11	46504	19	57370
4pipe	244	411107	263	382750

Results on some (unsatisfiable) problem instances from the Velev suite discussed at the beginning of Section 2.1 are shown in Table 1. As can be seen, performance is comparable; PBCHAFF pays a small (although noticeable) cost for its extended expressivity. The experiments were run on a 1.5 GHz AMD Athlon processor, and both solvers used the same values for the various tuning parameters available (relevance and length bounds, etc.).

Table 2: Run time (seconds) and nodes expanded

	ZCHAFF		Preprocess	PBCHAFF
Instance	sec	nodes	sec	sec	nodes
hole8.cnf	0	3544	0	0	11
hole9.cnf	1	8144	0	0	12
hole10.cnf	17	27399	0	0	17
hole11.cnf	339	126962	0	0	15
hole12.cnf			0	0	20
hole20.cnf			0	0	34
hole30.cnf			4	0	52
hole40.cnf			25	0	75
hole50.cnf			95	0	95

Results for the pigeonhole problem appear in Table 2. In this case, PBCHAFF was permitted to preprocess the problem using strengthening as described earlier in this section. ZCHAFF was unable to solve the problem for twelve or more pigeons with a 1000-second timeout using a 1.5 GHz Athlon processor. Not surprisingly, PBCHAFF with preprocessing dramatically outperformed ZCHAFF on these instances.¹³