---

Pbmodels --- software to compute stable models of logic programs with weight atoms

Introduction

Benchmark

Experimental results

Download package

Authors

References

Related links

---

What's New?

• 2006.02.26: A new release of pbmodels is available. Now it accepts three more PB solvers: minisat+, pueblo, and pbs4. For more information, please see the README file in the package and the links at the end of page.

---

Introduction

Pbmodels is a software to compute stable models of logic programs with weight atoms. We call such programs smodels programs, as we adopt for them the semantics implemented in smodels [1]. The key idea behind pbmodels is to translate programs into propositional theories and use propositional satisfiability solvers. However, unlike existing systems assat [2] and cmodels [3], which first exploited this direction, we do not replace weight atoms with propositional formulas. Instead, we translate programs with weight atoms directly into theories in propositional logic extended with weight atoms, which we refer to as the logic PL^wa [4]. We then use existing solvers for such theories, which we refer to as PB solvers, as computational back-end engines. In some cases, prior to the use of a PB solver, additional simple transformations are needed to ensure the right input format.

Compiling away weight atoms may lead to significantly larger programs and theories. Currently most advanced translations result in the growth by a logarithmic factor in the case of cardinality atoms, and a polynomial factor in the case of general weight atoms. Moreover, for some solvers, especially those based on the local-search idea, the structure of the resulting theories makes them difficult to process. Pbmodels is designed to compute models of smodels programs without compiling weight atoms away. The theoretical foundation was established in [4] and [5].

The PB solvers that pbmodels currently supports include: aspps [6], satzoo [7], pbs [8], wsatcc [9], wsatoip [10], and saturn [11].

Back to Top

Benchmark

This section shows the experimental results that compare the performance of pbmodels, cmodels, and smodels. We used the aspps, satzoo, pbs, wsatcc, and wsatoip in the following experiments. All experiments were run on machines with single 3.2GHz Pentium 4 CPU, 1GB memory, running Linux with kernel version 2.6.11 and gcc version 3.3.4.

We considered the following benchmark problems: traveling salesperson problem, weighted n-queens problem, weighted latin-square problem, magic square problem, vertex cover problem, and tower-of-hanoi problem. The first four problems require the use of general weight atoms in their logic programs, while the last two problems only need cardinality atoms.

traveling salesperson problem:

An instance of this problem is a pair (G, w), where G is a weighted complete graph (each edge has a positive integer weight) and w is an integer bound. A solution to the instance is a Hamilton cycle whose weight (the sum of the weights of the edges in the Hamilton cycle) is less than or equal to w.

We randomly generated 50 weighted complete graphs containing 20 vertices. The weights of edges are chosen unformly from the set of integers {1, ... ,19}. We then created two sets of instances using the weighted graphs by setting w to 100 and 62 respectively. We call the first set the easy case since all instances have solutions. We call the second set the hard case since only about half of the instances can be solved by some solver within the 3000 seconds time limit. The other half of the instances, which cannot be solved by any solvers, may still possess solutions. We name the instances of the following benchmarks as easy and hard instances with the same intension.

weighted n-queens problem:

An instance of this problem is a pair (B, w), where B is a n by n weighted chessboard (each cell has a positive integer weight) and w is an integer bound. A solution to the instance is a placement of n queens on the chessboard so that 1) no two queens are attacking each other and 2) the weight of the placement (the sum of the weights of the cells that are occupied by queens) is less than or equal to w.

We randomly generated 50 weighted chessboards of size 20 by 20. The weights are drawn uniformly from the set of integers {1, ... , 19}. The set of easy instances has w = 70. The set of hard instances has w = 50.

weighted latin square problem:

An instance of this problem is a pair (B, w), where B is a n by n weighted board (each cell has a positive integer weight) and w is an integer bound. A solution to the instance is a placement of integers 1 to n on the board so that 1) each number occurs exactly once along each row and column and 2) the weight of the placement (the sum of the weight of the cell times the number in that cell) is less than or equal to w.

We randomly generated 50 weighted boards of size 10 by 10. The two sets of instances (easy ones and hard ones) were created by setting w to 250 and 225 respectively.

magic square problem:

An instance of this problem is a n by n board. A solution to the instance is a placement of integers 1 to n on the board so that the sums of the numbers on each row, each column, the ascending diagonal, and the descending diagonal are the same.

We tested the target solvers on instances of size 4 by 4, 5 by 5, and 6 by 6. The encoding of this problem uses general weight atoms.

vertex cover problem:

An instance of this problem is a pair (G, k), where G=<V,E> is an undirected graph and k is an integer bound. A solution to the instance is a subset V' of the set V of vertices such that for every edge in E, at least one end of the edge is in the V'. Furthermore, the size of V' is less than or equal to k.

We randomly generated 50 graphs containing 80 vertices and 400 edges. The bound k for each graph is set to the size of its minimum vertex cover. Therefore, each instance has solutions.

tower-of-hanoi problem:

The tower-of-hanoi problem consists of three towers and d disks of different sizes. Initially, all d disks are on the first tower. A solution is a plan that moves all disks to the third tower with the help of the second tower so that 1) only one disk can be moved at a time; 2) only the disk on top can be moved; and 3) no disk can be put onto a disk that is smaller than it. It is known that, for d disks, there is always a plan consisting of 2^d-1 steps.

We generated instances of this problem by setting the initial disk placement to the state so that there exists a t<=2^d-1 step plan. That is, an instance starts from the middle of the complete plan and a solution is to finish it from that starting point. We considered the following instances: (d=6, t=31), (d =6, t=36), (d =6, t=41), (d =6, t=63), and (d =7, t=127).

Back to Top

The following table shows the experimental results. There are also links to the logic programs we used and the instances we generated.

Benchmarks	Experimental Results
TSP lparse encoding (does not include weight assignments)	Easy Instances (n=20,w=100) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All		v.s. Complete		Mean		Median
	smodels		45/50			3		17		124.21		24.56
	pbmodels-satzoo		50/50			5		30		42.54		17.73
	pbmodels-pbs		18/50			2		3		210.19		163.23
	pbmodels-wsatcc		32/50			7		-		35.67		0.98
	pbmodels-wsatoip		47/50			34		-		14.53		0.47
	Hard Instances (n=20,w=62) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All		v.s. Complete		Mean		Median
	smodels		19/50			1		7		1558.37		1637.14
	pbmodels-satzoo		19/50			2		16		696.42		461.25
	pbmodels-pbs		1/50			0		0		1482.24		1482.24
	pbmodels-wsatcc		19/50			6		-		28.39		6.59
	pbmodels-wsatoip		28/50			22		-		7.20		1.43
Weighted n-queens lparse encoding (does not include weight assignments)	Easy Instances (n=20,w=70) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All	v.s. Complete			Mean		Median
	smodels		11/50			0	5			520.28		499.58
	pbmodels-satzoo		26/50			0	23			425.37		382.59
	pbmodels-pbs		0/50			0	0			N/A		N/A
	pbmodels-wsatcc		49/50			45	-			0.14		0.11
	pbmodels-wsatoip		49/50			4	-			0.29		0.27
	Hard Instances (n=20,w=50) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All	v.s. Complete			Mean		Median
	smodels		2/50			0	2			697.81		661.20
	pbmodels-satzoo		0/50			0	0			N/A		N/A
	pbmodels-pbs		0/50			0	0			N/A		N/A
	pbmodels-wsatcc		29/50			15	-			1.01		0.33
	pbmodels-wsatoip		29/50			14	-			0.44		0.35
Weighted latin-square lparse encoding (does not include weight assignments)	Easy Instances (n=10,w=280) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All	v.s. Complete			Mean		Median
	smodels		21/50			0	1			11.30		0.67
	pbmodels-satzoo		49/50			3	29			44.68		0.25
	pbmodels-pbs		46/50			1	19			51.18		0.50
	pbmodels-wsatcc		45/50			33	-			0.24		0.05
	pbmodels-wsatoip		45/50			14	-			0.11		0.08
	Hard Instances (n=20,w=225) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All	v.s. Complete			Mean		Median
	smodels		0/50			0	0			N/A		N/A
	pbmodels-satzoo		47/50			20	26			278.80		189.14
	pbmodels-pbs		46/50			20	23			279.81		207.62
	pbmodels-wsatcc		7/50			1	-			1.10		0.57
	pbmodels-wsatoip		8/50			7	-			0.34		0.11
Vertex cover lparse encoding	Instances (80 vertices, 400 edges) original data RTD table RTD plot		# of Instances Solved			# of Times Won				Timing
						v.s. All	v.s. Complete			Mean		Median
	smodels		50/50			0	40			1.84		1.46
	cmodels		50/50			0	6			96.27		20.08
	pbmodels-satzoo		50/50			0	1			12.43		6.31
	pbmodels-pbs		46/50			0	3			199.66		70.82
	pbmodels-aspps		50/50			0	0			26.13		22.63
	pbmodels-wsatcc		50/50			36	-			0.32		0.03
	pbmodels-wsatoip		50/50			15	-			0.07		0.05
Magic square lparse encoding generator for different sizes	Size	smodels			cmodels	pbmodels-satzoo			pbmodels-pbs		pbmodels-aspps
	4X4	1.36			N/A	1.70			2.41		N/A
	5X5	> 1000			N/A	28.13			0.31		N/A
	6X6	> 1000			N/A	75.58			> 1000		N/A
Tower-of-hanoi lparse encoding	Size	smodels			cmodels	pbmodels-satzoo			pbmodels-pbs		pbmodels-aspps
	d=6,t=31	16.19			> 1000	18.47			1.44		9.14
	d=6,t=36	32.21			> 1000	31.72			1.54		60.00
	d=6,t=41	296.32			> 1000	49.90			3.12		240.24
	d=6,t=63	> 1000			> 1000	> 1000			3.67		> 1000
	d=7,t=127	> 1000			> 1000	> 1000			22.83		> 1000

Back to Top

Download package

The most recent version (12/28/2006): pbmodels-0.2.tar.gz

The next version (coming soon): Next version will support all PB solvers that accept inputs in "opb" format

Back to Top

Authors

Lengning Liu and Mirosław Truszczyński

Back to Top

References

1. Niemelä, I., Simons, P.: Extending the smodels system with cardinality and weight constraints. In Minker, J., ed.: Logic-Based Artificial Intelligence. Kluwer Academic Publishers (2000) 491 -- 521.

2. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Proceedings of AAAI-2002, AAAI Press (2002) 112 -- 117.

3. Babovich, Y., Lifschitz, V.: Cmodels package (2002) http://www.cs.utexas.edu/users/tag/cmodels.html

4. Liu, L., Truszczyński, M.: Properties of programs with monotone and convex constraints. In: Proceedings of AAAI-2005 To appear.

5. Marek, V., Truszczyński, M.: Logic programs with abstract constraint atoms. In: Proceedings of AAAI-04, AAAI press (2004), 86 -- 91.

6. East, D., Truszczyński, M.: Predicate-calculus based logics for modeling and solving search problems. ACM Transactions on Computational Logic (2004) To appear, available at http://www.acm.org/tocl/accepted.html

7. Eén, N., Sörensson, N.: An extensible SAT solver. In: Proceedings of SAT-2003. Volume 2919 of LNCS., Springer (2003) 502 -- 518.

8. Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: a backtrack-search pseudo-boolean solver and optimizer. In: Proceedings of SAT-2002, 346 -- 353.

9. Liu, L., Truszczyński, M.: Local-search techniques in propositional logic extended with cardinality atoms. In: Proceedings of CP-2003, volumn 2833 of LNCS., Springer (2003) 495 -- 509.

10. Walser, J.: Solving linear pseudo-boolean constraints with local search. In: Proceedings of AAAI-1997, AAAI Press (1997) 269 -- 274.

11. Prestwich, S.: Randomized backtracking for linear pseudo-boolean constraint problems. In: Proceedings of CPAIOR-2002, 7 -- 20.

Back to Top

Related links

smodels: http://www.tcs.hut.fi/Software/smodels

cmodels: http://www.cs.utexas.edu/users/tag/cmodels.html

assat: http://assat.cs.ust.hk/

satzoo: http://www.cs.chalmers.se/~een/Satzoo/

pbs: http://www.eecs.umich.edu/~faloul/Tools/pbs/

aspps: http://www.cs.uky.edu/ai/aspps/

wsatcc: http://www.cs.uky.edu/ai/wsatcc/

wsatoip: http://www.ps.uni-sb.de/~walser/wsatpb/wsatpb.html

saturn: somewhere on http://www.4c.ucc.ie/

asparagus: http://asparagus.cs.uni-potsdam.de/

ASPLIB: http://dit.unitn.it/~wasp/index.html

PBLIB: http://www.cirl.uoregon.edu/PBLIB/

PB competition 2005: http://www.cril.univ-artois.fr/PB05/

minisat+: http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

pueblo: http://www.eecs.umich.edu/~hsheini/pueblo/

pbs4: http://www.eecs.umich.edu/~faloul/Tools/pbs4/

Back to Top

---