Minimal Model Generation with respect to an Atom Set

Abstract

This paper studies minimal model generation for SAT instances. In this study, we minimize models with respect to an atom set, and not to the whole atom set. In order to enumerate minimal models, we use an arbitrary SAT solver as a subroutine which returns models of satisfiable SAT instances. In this way, we benefit from the year-byyear progress of efficient SAT solvers for generating minimal models. As an application, we try to solve job-shop scheduling problems by encoding them into SAT instances whose minimal models represent optimum solutions.

Introduction

The notion of minimal Herbrand models is important in a wide range of areas such as logic programming, deductive database, software verification, and hypothetical reasoning. Some applications would actually need to generate minimal models of a given formula.

In this work, we consider the problem of automating propositional minimal model generation with respect to an atom set. Some earlier works [ 3, 14, 9 ] considered minimal model generation with respect to the whole atom set.

Bry and Yahya [ 3 ] presented a sound and complete procedure for generating minimal models. They incorporate complement splitting and constrained search into positive unit hyper-resolution in order to reject nonminimal models. Niemela¨ [ 14 ] also gave a sound and complete procedure. His method is based on a generate and test method: generate a sequence of minimal model candidates and reject nonminimal models by groundedness test which passes minimal models. Hasegawa et al. [ 9 ] presented an minimal model generation method employing branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models.

However, these earlier works do not make use of some pruning techniques such as non-chronological or intelligent backtracking, and generating lemmas. These techniques make reasoning systems practical ones. In recent years, the ⋆ This work was supported by KAKENHI (20240003). propositional satisfiability (SAT) problem has been studied actively [ 1 ]. Specially, many works for implementing efficient SAT solvers have been performed in the last decade. The state-of-the-art SAT solvers can solve SAT problems consisting of millions of clauses in a few minutes. Then, it has been realized that we solve several kinds of problems by encoding them into SAT problems [ 7, 2 ].

This paper shows a method to generate minimal models with a SAT solver. Thus, the method benefits from the year-by-year progress of SAT solvers implementing the pruning techniques efficiently. We also try to solve the job-shop scheduling problems (JSSP) in the minimal model generation framework, in which, minimal models represent optimum, namely, the shortest schedules.

The remaining part of this paper is organized as follows: First we present a characterization of minimal models that is the key to our method to handle minimal model generation. Section 3 gives minimal model inference procedures with a SAT solver. Section 4 describes the job-shop scheduling problem and encodes it as a SAT instance. Section 5 demonstrates that the procedures are successfully implemented with the SAT solver MiniSat 2 by solving several JSSPs. We end the paper with a short summary and a discussion of future works. 2

Properties of Minimal Models

Models of a propositional formula can be represented by a set of propositional variables (or atoms); namely, each model is represented by the set of propositional variables to which it assigns true. For example, the model assigning true to a, false to b, and true to c is represented by the set {a, c}. In this representation, we can compare two models by set inclusion. For example, model {a, c} is smaller than model {a, b, c}. In this study, we focus on minimality of models in the representation.

Definition 1. Let P , M1 and M2 be atom sets. Then, M1 is said to be smaller than M2 with respect to P if M1 ∩ P is a proper subset of M2 ∩ P . Example 1. Let M1 = {p1, p2, p3, a}, M2 = {p1, p3, b, c, e, f } and P = {p1, p2, p3}. Then, M2 is smaller than M1 with respect to P .

Definition 2 (Minimal model). Let A be a propositional formula, P be an atom set, and M be a model of A. Then, M is said to be a minimal model of A with respect to P when there is no model smaller than M with respect to P . Example 2. Let A be a propositional formula and P = {p1, p2, p3}. And, A has three models M1 = {p1, p2, p3, a}, M2 = {p1, p2, b}, and M3 = {p3, c}. Then, M2 and M3 are minimal models with respect to P while M1 is not minimal.

This definition is the same as that of circumscription Circum(A(P, Z); P ; Z) [ 10 ] when variable predicates Z = P , i.e. no fixed predicate. Note that P denotes the set complement of P . In this sense, our study is a specialized one of circumscription. There is a little difference between our work and circumscription for the treatment of models. We are interested only in truth values of atoms in P . Therefore, we regard two models M1 and M2 as equal when M1 ∩ P = M2 ∩ P , while these two are distinguished in the framework of circumscription when M1 6= M2.

The following theorem is a straight extension of Proposition 6 in Niemela¨’s work [ 14 ]. This theorem gives the basis of the computational treatment of minimal models as Proposition 6 does.

Theorem 1. Let A be a propositional formula, P be an atom set, and M be a model of A. Then, M is a minimal model of A with respect to P iff a formula A∧ ¬(a1∧a2∧. . .∧am)∧¬b1∧¬b2∧. . .∧¬bn is unsatisfiable, where {a1, a2, . . . , am} = M ∩ P and {b1, b2, . . . , bn} = M ∩ P .

Proof. Let G be A ∧ ¬(a1 ∧ a2 ∧ . . . ∧ am) ∧ ¬b1 ∧ ¬b2 ∧ . . . ∧ ¬bn. Assume that M is not a minimal model. Then, there is a model N smaller than M with respect to P . Thus, the following properties hold: ∀j(1 ≤ j ≤ n)(N |= ¬bj ) and ∃i(1 ≤ i ≤ m)(N |= ¬ai). Of course, N |= A because N is a model of A. Therefore, N |= G; namely G is satisfiable.

Conversely, we assume G is satisfiable. Then, there is a model N such that ∀j(1 ≤ j ≤ n)(N |= ¬bj ) and ∃i(1 ≤ i ≤ m)(N |= ¬ai). This implies N is smaller than M with respect to P . That is, M is not a minimal model with respect to P .

Example 3. Let A be a propositional formula and P = {p1, p2, p3, p4}. Then, a model {p1, p4, c, d} of A is minimal with respect to P iff A∧¬(p1 ∧p4)∧¬p2 ∧¬p3 is unsatisfiable. 3

Procedures

This section gives procedures for generating minimal models of a SAT instance with a SAT solver based on the generate and test method: generating a sequence M1, . . . , Mi, . . . of models and performing minimality test on each Mi. In these procedures, we use a single SAT solver as both generator and tester where we assume the SAT solver returns a model of a satisfiable SAT instance. Almost all SAT solvers satisfy this assumption.

Figure 1 (a) shows a minimal model generation with respect to an atom set P which is implicitly given to the procedure. We call this the naive version. A0 is a SAT instance to be proved. The function solve(A) denotes the core part of the SAT solver. The function returns false when a SAT instance A is unsatisfiable and true when A is satisfiable. In the latter case, a model M of A is obtained through an array from which we construct two formulas F1 and F2 for a minimality test on M with respect to P where F1 = ¬(a1 ∧ . . . ∧ am) and F2 = ¬b1 ∧ . . . ∧ ¬bn. A boolean variable exhaustive indicates whether the procedure generates all minimal models or only one minimal model. If exhaustive is set to true, all minimal models are generated.

If solve(A) in line (2) returns true, the body of the while statement is executed. In this case, as a model M of A is obtained, we perform a minimality test on M (in (4)). If the test passes, that is solve(A) in (4) returns f alse, we conclude M is minimal with respect to P . If the test fails or exhaustive is true, F1 is added to A1 as a conjunct in order to avoid generating the same model or larger models in succeeding search. Thus, the role of the conjunct F1 is pruning redundant models. that ∃i(1 ≤ i ≤ m)(ai 6∈ SM). Therefore, at least one current ¬ai participates in F2 of the next minimize.

The major difference between the naive version and the normal version is the use of SM obtained from the minimality test. The naive version ignores it while the normal version uses it. Therefore, we expect that the normal version is more efficient than the naive version for enumerating minimal models. 3.1

Lemma Reusing

Many state-of-the-art SAT solvers learn lemmas called conflict clauses to prune redundant search space, but lemmas deduced from a certain SAT instance can not apply to solve other SAT instances. Therefore, a function call solve(A) in Figure 1 (both (a) and (b)) can not use lemmas deduced from previous solve(A) in general.

However, every SAT instance A in solve(A) satisfies the following lemmareusability condition [ 13 ] if the conjunct F1 is not added to A, when the SAT solver uses Chaff-like lemma generation mechanism [ 12 ].

Definition 3 (Lemma-reusability condition [ 13 ]). Suppose that A and B are SAT instances. The lemma-reusability condition between A and B is as follows: If A includes a non-unit clause x, then B contains x.

If both A and B satisfy the condition, we can use lemmas generated by solve(A) for solve(B). This is justified by the following proposition which is a paraphrase of Theorem 1 in [ 13 ].

Proposition 1. If A is a SAT instance and c is any lemma generated by solve(A), then c is a logical consequence of a set of some non-unit clauses in A.

This proposition is true when we use the SAT solver MiniSat for implementing solve(A), because MiniSat does not use any unit clause for generating lemmas.

F1 is a non-unit clause and violates the lemma-reusability condition. However, the only role of F1 is excluding models larger than the model causing F1. Then, lemmas depending on F1 can be used for succeeding minimal model generation. It follows from what has been said that every call solve(A) shares lemmas each other. 3.2

An Implementation with MiniSat

We have implemented the minimal model generation procedures with the SAT solver MiniSat [ 5 ] version 2.1 which is written in C++. MiniSat 2.1 took the first place in the main track of SAT-Race 2008.

The solve method of MiniSat is declared as follows: bool solve(const vec<Lit>& assumps)

The method determines the satisfiability of a set of clauses under an assumption assumps. It returns true if the set is satisfiable; otherwise false. The clause set is realized by a vector clauses and initialized to a SAT instance (A0 in Figure 1). The assumption assumps is a vector of literals which means the conjunction of the literals.

In our implementation, the clause F1 is appended to clauses and the formula F2 is set to assumps. Then, the solve method is invoked. We don’t need to remove F1 from clauses before the next solve invocation because the role of F1 is excluding models larger than the model causing F1. If F2 is appended to clauses, we need to remove F2 from clauses before the next invocation. Therefore, we add F2 to assumps instead of clauses. Thus, removing F2 is not necessary.

When we need only one minimal model3 rather than all minimal models, we can append F2 to clauses without removing F2 afterward. We also implement such solver based on the normal version and call it the single-solution version. 4

Solving the JSSP

A JSSP consists of a set of jobs and a set of machines. Each job is a sequence of operations. Each operation requires the exclusive use of a machine for an uninterrupted duration, i.e. its processing time. A schedule is a set of start times for each operation. The time required to complete all the jobs is called the makespan. The objective of the JSSP is to determine the schedule which minimizes the makespan.

In this study, we follow a variant of the SAT encoding proposed by Crawford and Baker [ 4 ]. In the SAT encoding, we assume there is a schedule whose makespan is at most i and generate a SAT instance Si. If Si is satisfiable, then the JSSP can complete all the jobs by the makespan i. Therefore, if we find a positive integer k such that Sk is satisfiable and Sk−1 is unsatisfiable, then the minimum makespan is k.

For minimizing the makespan, Nabeshima et al. [ 13 ] applied two kinds of methods, incremental search and binary search. One can easily estimate the upper bound Lup of the minimum makespan by serialising all the operations of all the jobs 4. The lower bound Llow is also easily estimated by taking the maximum length of each job in which we assume every job is performed independently. In the incremental search, we start from Llow and increase the makespan by 1 until we encounter the satisfiable instance St. If such St is found, then the minimum makespan is t. We explain the binary search by an example of Lup = 393 and Llow = 49. Firstly, we try to solve S221 because 221 is the midpoint between 48 and 393. If S221 is satisfiable, then try S135. If S135 is unsatisfiable, then try S178. We continue this binary search until we encounter the satisfiable instance St and unsatisfiable instance St−1. 3 The JSSP is such a problem. 4 In this study, we use a modified estimation a bit cleverer than this obvious estimation.

In order to solve the JSSP in the minimal model generation framework, we introduce a set Pu = {p1, p2, . . . , pu} of new atoms when Lup = u. The intended meaning of pi = true is that we found a schedule whose makespan is i or longer than i. To realize the intention, the formulas Fi(i = 1, . . . , u), which represent “if all the operations complete at i, then pi becomes true,” are introduced. Besides, we introduce a formula Tu = (¬pu ∨ pu−1) ∧ (¬pu−1 ∨ pu−2) ∧ · · · ∧ (¬p2 ∨ p1) which implies that ∀l(1 ≤ l < k)(pl = true) must hold if pk = true holds.

In this setting, if we obtain a model M of Gu(= Su ∧ F1 ∧ · · · ∧ Fu ∧ Tu) and k is the maximum integer such that pk ∈ M , that is, ∀j(k < j ≤ u)(pj 6∈ M ), then we must have ∀l(1 ≤ l ≤ k)(pl ∈ M ), namely, M ∩ Pu = {p1, . . . , pk}. The existence of such k is guaranteed by Fk and Tu, and indicates that there is a schedule whose makespan is k. If k is the minimum makespan, there is no model of Gu smaller than M with respect to Pu. Thus, a minimal model of Gu with respect to Pu represents a schedule which minimizes the makespan. Example 4. Given a JSSP with Lup = 10. Then, we make S10 according to Crawford encoding, P10 = {p1, . . . , p10}, and T10 = (¬p10 ∨ p9) ∧ · · · ∧ (¬p2 ∨ p1). Let M be a minimal model of G10(= S10 ∧ F1 ∧ · · · ∧ F10 ∧ T10) with respect to P10 and M ∩ P10 = {p1, p2, p3}. Then, the minimum makespan of the JSSP is 3.

This SAT encoding technique, in which a minimal model represents an optimum solution, is applicable to several problems such as graph coloring problem, open-shop scheduling problem, two dimensional strip packing problem, and so on. Thus, the technique gives a framework to solve these problems.

The encoding is easily adapted for a partial Max-SAT encoding by adding some unit clauses. Max-SAT is the optimization version of SAT where the goal is to find a model satisfying the maximum number of clauses. In order to solve the JSSP in the partial Max-SAT framework5, we introduce u unit clauses ¬pi(i = 1, . . . , u). Then, we solve M AXu(= Gu ∧¬p1 ∧. . .∧¬pu) with a partial Max-SAT solver where all clauses in Gu are treated as hard clauses and ¬pi(i = 1, . . . , u) are as soft clauses. A Max-SAT model of M AXu represents a optimum schedule. Example 5. Let P10, G10, and M be the same as in Example 4. Then M AX10 = G10 ∧ ¬p1 ∧ . . . ∧ ¬p10 has a (Max-SAT) model M which falsifies only three soft clauses ¬p1, ¬p2, and ¬p3. Note that every model of G10 falsifies at least these three clauses. 5

Experiments

We executed the three versions(naive/normal/single-solution), a Max-SAT solver MiniMaxSat[ 6 ], and a SAT-based JSSP solver SATSHOP which is a successor of 5 A partial Max-SAT solver can handle hard clauses and soft clauses. The hard clauses must be satisfied while the soft clauses need not be necessarily satisfied. The goal is to find a model satisfying the all hard clauses and the maximum number of soft clauses. the JSSP solver proposed in [ 13 ]. The MiniMaxSat took the third place in the partial Max-SAT category (industrial) of Max-SAT Evaluation 2008.

The SATSHOP tries to solve a JSSP in the following way. First, making a relaxed problem to improve the upper bound Lup. The relaxed problem is an approximation of the original problem. It is obtained by rounding up every operation time. Its optimum solution gives a new upper bound Lunpew which satisfies Lunpew ≤ Lup. The relaxed problem is solved with the SAT encoding technique using binary search.

Next, solving the problem with Lunpew by decremental search. Basically, decremental search is a dual of incremental search. We start from Lunpew and decrease the makespan until we encounter the unsatisfiable instance.

We try to solve 82 JSSPs in OR-Library [ 15 ]. The problems are abz5–abz9, ft06, ft10, ft20, la01–la40, orb01–orb10, swv01–swv20, and yn1–yn4. We limited the execution time of each problem to 2 CPU hours. The single-solution version and SATSHOP succeed to solve 33 problems out of 82 problems. The naive version, normal version, and MiniMaxSAT succeed to solve 32, 31, and 14 problems, respectively. Table 1 shows the experimental results of 33 problems solved.

All experiments were conducted on a Pentium M 753(1.20GHz) machine with 1GB memory running Linux 2.6.16. Each problem is encoded to a CNF (conjunctive normal form)6. The second and third columns show statistics of CNFs. The fourth column “|P |” shows the size of an atom set P with respect to which we minimize a model. The fifth column “Optimum” shows the minimum makespan. “Single” is the single-solution version. The “Total” row shows the total CPU time for the single-solution version or SATSHOP. The “Ratio” row shows (total time of SATSHOP)/(total time of Single).

The single-solution version usually beats other two versions as expected. On average it solves problems 1.6 times faster than the naive version and 1.3 times faster than the normal version for the 31 problems solved by these three versions.

On the other hand, the SATSHOP beats these three versions on almost all problems. On average it solves problems about 1.7 times faster than the single-solution version. The main reason for the domination of the SATSHOP is that it tries to solve a relaxed problem first. The relaxed one is easy to solve by orders of magnitude. In order to eliminate the effect of the relaxation, we also run the SATSHOP in a non-relaxation mode where it try to solve JSSPs without relaxation. This causes an increase of the runtime of the SATSHOP. The single-solution version, then, is almost comparable with the SATSHOP: the former sometimes beats the latter, and vice versa. On average, the latter solves problems about 1.2 times faster than the former.

The MiniMaxSAT is the worst solver in our experience. It can solve only half of problems solved by others within 2 CPU hours. It seems to be several hundred times slower than others. We may need to develop a SAT encoding tailored for MaxSAT solvers. 6 We also use the SATSHOP as an encoder. Thus, the core part of a SAT instance solved by the three versions is the same one solved by the SATSHOP.

Turning now to the 49 problems unsolved within 2 CPU hours, even their 48 relaxed problems can not be solved by SATSHOP. Furthermore, some SAT instances are huge 7 for our experimental environment. Ten of the 49 instances require more than 1GB memory, and five of the ten require more than 4GB memory which a 32-bits CPU can not manipulate any more. 6

Conclusions and Future Work

In this paper we presented a characterization of a minimal model with respect to an atom set. Based on this characterization, we gave minimal model generation procedures using a SAT solver as a subroutine. The only function we require from the SAT solver is to compute a model of a satisfiable SAT instance. Thus, our implementation benefits from efficiency of state-of-the-art SAT solvers.

We implemented the naive, normal, and single-solution versions with the SAT solver MiniSat 2. We have performed an experimental evaluation with 82 JSSPs. It shows that the single-solution version usually beats the other two versions. Unfortunately, it rarely beats the SAT-based JSSP solver SATSHOP which performs several optimizations concerning the problem domain. It is for this reason that the SATSHOP generally beats others. In spite of the domination of the SATSHOP, the minimal model generation approach still has an advantage over the SATSHOP in the sense that the former is more general than the latter: the latter solve only JSSP while the former can solve not only JSSP but also several problems such as graph coloring problem, two dimensional strip packing problem, and so on. Stochastic SAT solvers, such as WalkSAT [ 17 ], may be useful for increasing performance of the three versions.

We have also applied the Max-SAT solver MiniMaxSAT to the 82 JSSPs. The experimental results show that the MiniMaxSAT is definitely inefficient for solving the JSSP in our SAT encoding though it is a state-of-the-art MaxSAT solver. Implementing a Max-SAT solver based on our approach looks like interesting future work.

Some problems can not be solved because of memory capacity. In order to solve these problems in our framework, we have to purchase a 64-bits CPU and memory, or develop methods to manipulate the problem on the available memory. Encoding the problem into a first order formula seems to be a promising approach to save memory [ 16 ].

Answer set programming launched out into the new paradigm of logic programming in 1999, in which a logic program represents the constraints of a problem and its answer sets correspond to the solutions of the problem [ 11 ]. Computing answer sets is realized by generating minimal models and checking whether they satisfy some conditions for negation as failure [ 8 ]. We plan to extend this work to computing answer sets. 7 SWV13 has the hugest instance in our experiment. It has 2.4 million variables and 121.6 million clauses. And its DIMACS file in gzip format occupies 596 MB.

References

1. L. Bordeaux , Y. Hamadi , and L. Zhang: Propositional Satisfiability and Constraint Programming: A Comparative Survey . ACM Computing Surveys , Vol. 38 , No.4, Article 12 ( 2006 )

2. A. Biere , A. Cimatti , E. M. Clarke , and Y. Zhu : Symbolic Model Checking without BDDs . In Proc. of TACAS'99 , pp. 193 - 207 ( 1999 )

3. F. Bry and A. Yahya : Minimal Model Generation with Positive Unit Hyperresolution Tableaux . In Proc. of TABLEAUX'96 , pp. 143 - 159 ( 1996 )

4. J. M. Crawford , A. B. Baker : Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems . In Proc. of AAAI-94 , pp. 1092 - 1097 ( 1994 )

5. N. E´en and N. S¨orensson: An Extensible SAT-solver . In Proc. of SAT-2003 , pp. 502 - 518 ( 2003 )

6. F. Heras , J. Larrosa , and A. Oliveras: MiniMaxSAT: An Efficient Weighted MaxSAT Solver . J. of Artificial Intelligence Research , Vol. 31 , pp. 1 - 32 ( 2008 )

7. H. Kautz and B. Selman: Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search . In Proc. of AAAI-96 , pp. 1194 - 1201 ( 1996 )

8. K. Inoue , M. Koshimura , and R. Hasegawa : Embedding Negation as Failure into a Model Generation Theorem Prover . In Proc. of CADE-11 , pp. 400 - 415 ( 1992 )

9. R. Hasegawa , H. Fujita , and M. Koshimura: Efficient Minimal Model Generation Using Branching Lemmas . In Proc. of CADE-17 , pp. 184 - 199 ( 2000 )

10. V. Lifschitz: Computing Circumscription . In Proc. of IJCAI-85 , pp. 121 - 127 ( 1985 )

11. V. Lifschitz: Answer Set Planning . In Proc. of ICLP-99 , pp. 23 - 37 ( 1999 )

12. M. V. Moskewicz , C. F. Madigan , Y. Zhao , and L. Zhang: Chaff: Engineering an Efficient SAT Solver . In Proc. of DAC'01 , pp. 530 - 535 ( 2001 )

13. H. Nabeshima , T. Soh , K. Inoue , and K. Iwanuma: Lemma Reusing for SAT based Planning and Scheduling . In Proc. of ICAPS'06 , pp. 103 - 112 ( 2006 )

14. I. Niemel¨a: A Tableau Calculus for Minimal Model Reasoning . In Proc. of TABLEAUX'96 , pp. 278 - 294 ( 1996 )

15. OR-Library . http://people.brunel.ac.uk/~mastjjb/jeb/info.html

16. J. A. Navarro-P´ erez and A. Voronkov: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic . In Proc. of CADE-21 , pp. 346 - 361 ( 2007 )

17. B. Selman , H. Kautz , and B. Cohen : Local Search Strategies for Satisfiability Testing . Discrete Mathematics and Theoretical Computer Science , vol. 26 , AMS , ( 1996 )