What's New?
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].
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).
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 |
(n=20,w=100) original dataRTD 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 |
|||||||
(n=20,w=62) original dataRTD 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 |
(n=20,w=70) original dataRTD 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 |
|||||||
(n=20,w=50) original dataRTD 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 |
(n=10,w=280) original dataRTD 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 |
|||||||
(n=20,w=225) original dataRTD 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 |
(80 vertices, 400 edges) original dataRTD 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 |
Size |
smodels |
cmodels |
pbmodels-satzoo |
pbmodels-pbs |
pbmodels-aspps |
||||||
1.36 |
N/A |
1.70 |
2.41 |
N/A |
||||||||
> 1000 |
N/A |
28.13 |
0.31 |
N/A |
||||||||
> 1000 |
N/A |
75.58 |
> 1000 |
N/A |
||||||||
Tower-of-hanoi |
Size |
smodels |
cmodels |
pbmodels-satzoo |
pbmodels-pbs |
pbmodels-aspps |
||||||
16.19 |
> 1000 |
18.47 |
1.44 |
9.14 |
||||||||
32.21 |
> 1000 |
31.72 |
1.54 |
60.00 |
||||||||
296.32 |
> 1000 |
49.90 |
3.12 |
240.24 |
||||||||
> 1000 |
> 1000 |
> 1000 |
3.67 |
> 1000 |
||||||||
> 1000 |
> 1000 |
> 1000 |
22.83 |
> 1000 |
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
References
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.
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.
Babovich, Y., Lifschitz, V.: Cmodels package (2002) http://www.cs.utexas.edu/users/tag/cmodels.html
Liu, L., Truszczyński, M.: Properties of programs with monotone and convex constraints. In: Proceedings of AAAI-2005 To appear.
Marek, V., Truszczyński, M.: Logic programs with abstract constraint atoms. In: Proceedings of AAAI-04, AAAI press (2004), 86 -- 91.
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
Eén, N., Sörensson, N.: An extensible SAT solver. In: Proceedings of SAT-2003. Volume 2919 of LNCS., Springer (2003) 502 -- 518.
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: a backtrack-search pseudo-boolean solver and optimizer. In: Proceedings of SAT-2002, 346 -- 353.
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.
Walser, J.: Solving linear pseudo-boolean constraints with local search. In: Proceedings of AAAI-1997, AAAI Press (1997) 269 -- 274.
Prestwich, S.: Randomized backtracking for linear pseudo-boolean constraint problems. In: Proceedings of CPAIOR-2002, 7 -- 20.
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/