Automatic Generation of Implied Constraints Toby Walsh and Alan Frisch Artificial Intelligence Group University of York November, 1999 Case for Support A Background The aim of this project is to develop, analyse and evaluate methods for generating implied constraints automatically. We expect such methods to become a vital component of the next generation of constraint satisfaction toolkits. One of the key ideas will be to combine theorem proving techniques (like ordered resolution) with constraint satisfaction algorithms. Constraint satisfaction is a highly successful technology for tackling a wide variety of search problems including resource allocation, transportation and scheduling. As an example of the value of implied constraints, consider colouring the nodes in a graph so that adjacent nodes have different colours. This constraint satisfaction problem models a variety of assignment problems like exam and classroom timetabling. If we have a near k-clique in which all but one pair of k nodes are connected and k - 1 colours available, then we can infer an additional constraint that the two unconnected nodes must take the same colour. Adding this implied constraint explicitly to the problem representation could prevent a backtracking algorithm like forward checking from exploring an exponential number of partial colourings for the k nodes in the near k-clique. Several recent studies show that implied constraints added by hand to a problem representation can lead to significant reductions in search (e.g. [28]). There has, however, been little research on how to generate such implied constraints automatically outside of a highly focused domain like planning (see, for example, [10]). One exception is [12], which generalises resolution to multi-valued clauses (in which variables can take more than just the two values True and False), and proves that implied constraints generated by the closure of this operation will eliminate search. In practice, we cannot expect to eliminate search completely as the closure can be exponentially large to compute. One of the objectives of this research is to identify how much of the closure to generate to reduce the total time needed to solve a problem. Many inference techniques can be viewed as methods for generating restricted classes of implied constraints. For example, consistency techniques like arc-consistency generate implied unary constraints. As a second example, nogood recording techniques [8] generate implied constraints that are inferred from dead-ends in search. These techniques can give large reductions in search both on hard random problems [14] as well as on more realistic benchmarks [3, 4, 15]. Inference techniques in domains closely related to constraint satisfaction such as operations research (OR) and propositional satisfiability (SAT), can also be viewed as methods for generating implied constraints. For example, cutting planes in OR are highly effective at strengthening linear relaxations and at pruning search [24]. Cutting planes are implied constraints derived from the original set of inequalities. They are restricted to linear inequalities so that we can perform linear relaxation. Hooker has shown [24] that resolution (and its generalisation to multi-valued clauses) is a general method for generating cutting planes analogous to more traditional techniques like Chv'atal's method. As a final example, inference techniques in SAT such as directional resolution [9], can be highly competitive with more traditional branching techniques like the Davis-Putnam procedure [7]. Such methods generate resolvents which can again be viewed as implied constraints. B Programme and Methodology Programme of Work The aims of this project--the development, analysis and evaluation of methods for generating implied constraints automatically--are to be achieved through four major objectives. The first is to develop theorem proving techniques for generating implied constraints automatically. As such techniques are likely to generate both useful and unuseful constraints, the second objective is to develop heuristics for identifying which of the generated constraints to retain and which to discard. The first two objectives focus on the generation of constraints prior to the start of search. The third objective considers algorithms that interleave the generation of implied constraints with the search process itself. The fourth and final objective, which is the focus of a project studentship, is to apply these results to a closely related domain, propositional satisfiability (SAT) and some extensions of SAT. For each objective, we identify the sort of questions that we will address. In the workplan, we then list the work that will be performed to answer these questions. Objective 1: generating constraints automatically When representing a constraint satisfaction problem, implied constraints are typically generated by hand. We propose to explore several methods for automating this process. (1.1) generating constraints via theorem proving. Implied constraints are logical consequences of the initial problem. Is theorem proving therefore a suitable technology for generating implied constraints? To answer this question, we will encode the initial problem representation into a propositional theory and use standard theorem proving technologies like resolution [27] to generate implied constraints. We will attempt to determine the extent to which this approach is able to generate those constraints that have previously been added by hand. Many constraint satisfaction toolkits allow for specialised constraints like the all-different constraint [26]. Problems can often be represented more compactly and efficiently using such constraints [29]. How can we generate such implied constraints? We will explore several different routes. For example, can existing techniques like theorem proving be adapted to generate such non-binary constraints? How does this compare to specialised algorithms for generating such non-binary constraints? Chv'atal's method [24] is a popular OR technique for generating cutting planes and can be used to construct inequalities that follow from an initial problem representation. Is this a viable technique for generating implied constraints in constraint satisfaction? How do the theorem proving techniques we have developed compare to the approach of encoding the initial representation of the constraint satisfaction problem into a linear program, generating some cutting planes, and then mapping these back into constraints? (1.2) deciding when to generate implied constraints. Having developed some effective techniques for generating implied constraints, we must decide when to generate implied constraints. What features of a problem representation suggest that implied constraints can be usefully added to it? If we repeatedly generate implied constraints and add them to the problem representation, when should we stop? Again, we will explore several different routes. For example, can measures like the "constrainedness" of the problem representation [19] suggest when to add implied constraints? How does this depend on the constraint satisfaction algorithm to be used? For instance, it may pay to add more implied constraints when using a forward checking algorithm than when using an algorithm that maintains arc-consistency. Objective 2: identifying the value of implied constraints Having developed techniques for generating implied constraints and heuristics to decide when to use them, we must decide which of the generated constraints to add to the problem representation. Some implied constraints are "redundant" since they do not reduce search. As such constraints only add overhead, they should not be included in the representation. (2.1) assessing the value of implied constraints. We will again explore several different routes. For example, can we use the "constrainedness" of the constraint [19] to decide whether to add an implied constraint to the problem representation? Are other simpler measures like constraint size and tightness as effective? How does our decision depend on the constraint satisfaction algorithm to be used? (2.2) implied constraints for dynamic variable orderings. Given a fixed variable ordering, we can eliminate search if we generate implied constraints by an ordered form of resolution [12]. This result identifies the implied constraints sufficient to give backtrack free search, but which of these implied constraints is necessary? Can we give similar results for dynamic variable orderings? In practice, it will not pay to generate all the implied constraints. How then should we modify the generation and assessment of implied constraints to cope with dynamic variable ordering heuristics? Objective 3: using implied constraints within search The observation that consistency techniques like arc-consistency effectively generate implied unary constraints suggests that we may usefully generate implied constraints during the search process. (3.1) division of labour. How do we partition our effort between inference (generating implied constraints) and search? Recent empirical work has suggested that the hardest instances of search problems tend to occur around "phase transitions" in solubility [6, 19]. Can position in this phase space help us decide how to divide our labour? For example, it may be worth spending more time generating implied constraints for critically constrained problem instances close to the phase boundary than for under- or over-constrained problem instances away from the boundary. Instead of performing inference then search, can we interleave inference with search? As branching decisions will constrain the problem, new implied constraints could be generated as we descend the search tree. Perhaps the "constrainedness" of the current subproblem [19] can be used to decide when to attempt to generate more implied constraints? (3.2) implied constraints in local search. In SAT, the addition of implied clauses can improve the performance of local search procedures like GSAT [5]. In constraint satisfaction, can the addition of implied constraints improve the performance of local search procedures like min-conflicts? Are the heuristics we develop for controlling the generation of implied constraints for systematic search procedures also successful in the context of local search procedures? Objective 4: implied constraints in SAT In recent years, there has been considerable interest in encoding constraint satisfaction and other problems like planning into propositional satisfiability (SAT), and then using either an efficient complete procedure like Davis-Putnam or a fast semi-decision procedure like GSAT, WalkSAT. The success of such an approach often depends critically on the implied constraints included in the encoding [10]. Are the techniques developed for generating implied constraints for constraint satisfaction problems useful for generating implied constraints when encoding problems into SAT? (4.1) generating implied constraints in SAT. Can the techniques developed in (1.1) be used to generate implied constraints for SAT encodings? Are non-clausal languages (and generation techniques like non-clausal resolution) more effective than clausal languages? What about extensions to SAT like multi-valued clauses [13] (and the generalisation of resolution to multi-valued clauses [12]) and linear 0-1 constraints? Are lifted first-order languages with finite sorts (and generation techniques like full first-order resolution) more effective than propositional languages? What about even richer languages like modal and quantified Boolean formulae (QBF)? (4.2) deciding when to generate implied constraints in SAT. Can the results of (1.2) be used to decide when implied constraints can be usefully added to a SAT encoding? How does this depend on the SAT algorithm to be used? For instance, does it pay to add more implied constraints when using a Davis-Putnam procedure than when using a local search algorithm like GSAT? (4.3) assessing the value of implied constraints in SAT. Can the results of (2.1) be used to decide if an implied constraint is worth adding to the SAT encoding? How does the decision depend on the SAT algorithm to be used? Do the same methods work with richer languages like multi-valued clauses? Do the same results apply to richer problems like modal and QBF satisfiability? Work Plan and Milestones This project is expected to take three years. It will consist of four overlapping phases. The research assistant's effort will be dedicated to the first three phases, and the research student's to the fourth. The estimated time for each part of the project in person-months (pm) is as follows: (1.1) generating constraints via theorem proving (8pm). We will write an interface between a constraint solver like ILOG's Solver and the TPTP problem format. As this format is widely used within the theorem proving community (and as there exists a utility to convert it into many other formats), this interface will allow us to try many different theorem proving systems (like the Otter and Waldmeister provers) for generating the implied constraints. We will also write an interface between a constraint solver like ILOG's Solver and a standard OR language like AMPL. This will allow us to compare performance with off-the-shelf algorithms for generating cutting planes. In this, and the subsequent workpackages, we will compare the performance of the different techniques on problems taken from CSPLib. We will also look at techniques for generating specialised constraints, like the all-different and cardinality constraints. Such constraints occur widely in practical problems, and very efficient algorithms exist for enforcing consistency on these constraints. We will implement specialised algorithms for identifying such constraints. Such algorithms will necessarily be incomplete since, for example, identifying all-different constraints is equivalent to finding cliques in a graph, and this is NP-hard. We will also explore whether conventional theorem proving techniques can be adapted to infer such constraints. (1.2) deciding when to generate implied constraints (6pm). We will determine experimentally whether our "constrainedness" measure, Kappa [19] can be used to decide when to generate constraints. We will compare its performance to that of other measures, some much simpler like the number and tightness of the constraints. To explore the impact of the algorithm on such decisions, we will experiment with both a forward checking algorithm and an algorithm that maintains arcconsistency. (2.1) assessing the value of implied constraints (6pm). We will determine experimentally whether our "constrainedness" measure, Kappa can be used to decide whether an implied constraint is worth including adding to the problem representation. We will compare with other measures, some much simpler like the number and tightness of the implied constraint. To explore the impact of the algorithm on such decisions, we will again experiment with both a forward checking algorithm and an algorithm that maintains arc-consistency. (2.2) implied constraints for dynamic variable orderings (5pm). We will identify restrictions of resolution which give backtrack free search for a dynamic variable ordering. We will then study how the results of (1.1), (1.2) and (2.1) are affected by dynamic variable ordering heuristics. Our experiments will use simple heuristics like Fail-First, as well as more complex ones like Brelaz and the Kappa heuristic. (3.1) division of labour (6pm). We will determine experimentally whether position in the phase space can be used to decide whether to perform inference (generating implied constraints) or search. We will implement a procedure that interleaves inference and search, and test a variety of strategies for dividing effort between inference and search, including one based on the constrainedness of the (current) subproblem. (3.2) implied constraints in local search (5pm). We will test whether the heuristics developed in (1.2) and (2.1) for systematic procedures like forward checking are useful for local search procedures like min-conflicts. (4.0) literature survey and preliminary study (8pm). The aim of this part of the project is to bring the research student up to speed. A literature survey will be conducted on the use and generation of implied constraints within constraint satisfaction and SAT. A SAT solver like Davis-Putnam will be linked to the Otter theorem proving system (again using a TPTP style interface). In this and subsequent workpackages, experiments will be run using problems from the SATLIB and DIMACS benchmark libraries. (4.1) generating implied constraints in SAT (12pm). We will implement prototype systems for generating implied constraints using multi-valued resolution, non-clausal resolution, and full first-order resolution with finite sorts. We will compare results with the simple clausal system implemented in (4.0). We will also explore techniques for generating implied constraints in richer problems like modal and QBF satisfiability. (4.2) deciding when to generate implied constraints in SAT (8pm). We will determine experimentally whether our "constrainedness" measure, Kappa [19] can be used to decide when to generate constraints to add to the SAT encoding. We will compare with other measures, some much simpler like the number and length of the clauses. To explore the impact of the algorithm on such decisions, will experiment with both the Davis Putnam procedure and the WalkSAT local search algorithm. We will also explore this question in the context of richer problems like modal and QBF satisfiability. (4.3) assessing the value of implied constraints in SAT (8pm). We will determine experimentally whether our "constrainedness" measure, Kappa can be used to decide whether an implied constraint is worth including in the SAT encoding. We will again compare with other measures, some much simpler like the number and size of the implied clauses. To explore the impact of the algorithm on such decisions, we will again experiment with the Davis Putnam procedure and the NB-WalkSAT local search algorithm. We will also explore this question in the context of richer problems like modal and QBF satisfiability. There will be three milestones. At 12 months, the first milestone will be some conference papers comparing different approaches for generating implied constraints automatically. At 24 months, the second milestone will be some journal papers on generating implied constraints automatically, and identifying their potential value. At 36 months, the third and final milestone will be some journal papers on how to use implied constraints within both systematic and local search algorithms. A diagrammatic project plan appears at the end of this case for support. Timeliness and Novelty This proposal is highly original. There has been little research in constraint satisfaction on generating implied constraints automatically. This is surprising since implied constraints added by hand have been shown to offer significant reductions in search (e.g. [28]). It is therefore a very timely moment to devote more attention to this topic. Practical applications are likely to appear very quickly. Methodology The research methodology followed in this project is that of theoretical analysis backed up by large scale empirical tests. The availability of cheap and powerful computing resources means that we can run extensive computational experiments to confirm and add detail to theoretical results. We will therefore prototype the various technologies being explored, and test these implementations on the wide variety of problems found in CSPLib, the constraint satisfaction benchmark library set up and maintained by the first applicant. Such a mixture of theory and experiment has proved very successful in previous research carried out within the APES research group (see http://apes.cs.strath.ac.uk/ for more details). C Relevance to Beneficiaries Industrial Community Generating implied constraints automatically will improve our ability to solve constraint satisfaction and satisfiability problems quickly, and this is potentially of great commercial value. For example, this may allow problems to be solved in real time or more efficiently, leading both to reduced costs and increased quality. Areas such as resource allocation, transportation and scheduling problems are immediate application areas for the results of this research. The tools that will be developed during this project to generate and use implied constraints will increase the scope for decision support within commerce and industry, leading to an increase in competitive advantage of these businesses. The tools will be valuable in their own right since they can be used by companies like ILOG, and sold on within their constraint satisfaction toolkits. Academic Community The results of this research will be of considerable interest to the basic research community. Implied constraints added by hand have been shown to reduce search significantly. However, techniques for generating implied constraints automatically have not yet been investigated in any detail. We propose to correct this. The research will also help to bring together research in more theoretical areas like theorem proving with more applied areas like constraint satisfaction. D Dissemination and Exploitation Our results will be distributed by means of publications in the major journals and conferences, and via new software and benchmark problems. The applicants have been highly successful in disseminating results this way. These resources will also be distributed to the academic and industrial communities via WWW pages. We expect such resources will help improve the tools used to solve constraint satisfaction and satisfiability problems. For example, Dds, a novel search strategy proposed by one of the applicants [32] has recently been taken up by industry by this route, having been incorporated in ILOG's Solver constraint toolkit, and used by Thomson-CSF on a resource scheduling problem. We will liase with our industrial contacts like ILOG to identify similar routes for transferring results into their business. The University has a Research and Industry Office whose remit specifically includes technology transfer and licensing of research results. Should commercially exploitable results arise from the project, the Research and Industry Office will be approached to help with the technology transfer. References [1] D. Basin and T. Walsh. Difference unification. In Proceedings of the 13th IJCAI. International Joint Conference on Artificial Intelligence, 1993. [2] D. Basin and T. Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1-2):147-180, 1996. [3] Roberto Bayardo and Robert Schrag. Using CSP look-back techniques to solve exceptionally hard SAT instances. In Proceedings of Second International Conference on Principles and Practice of Constraint Programming (CP96), 1996. [4] Roberto Bayardo and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on AI. American Association for Artificial Intelligence, 1997. [5] B. Cha and K. Iwama. Adding new clauses for faster local search. In Proceedings of the 14th National Conference on AI, pages 332-337. American Association for Artificial Intelligence, 1996. [6] P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard problems are. In Proceedings of the 12th IJCAI, pages 331-337. International Joint Conference on Artificial Intelligence, 1991. [7] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394-397, 1962. [8] R. Dechter. Enhancement schemes for constraint processing: Backjumping, learning and cutset decomposition. Artificial Intelligence, 41(3):273-312, 1990. [9] R. Dechter and I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In Proceedings of KR-94, pages 134-145, 1994. A longer version is available from http://www.ics.uci.edu/~irinar. [10] M. Ernst, T.D. Millstein and D.S. Weld. Automatic SAT-Compilation of Planning Problems. In Proceedings of the 14th IJCAI, pages 1169-1177. International Joint Conference on Artificial Intelligence, 1997. [11] A.M. Frisch. The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning, Artificial Intelligence, 49(3):161-198, 1991. [12] A.M. Frisch. Solving Constraint Satisfaction Problems with NB-Resolution. In S. Muggleton, D. Michie and Luc De Raedt, editors, Machine Intelligence 16, 2000. Electronic Transactions in Artificial Intelligence. Available from http://www.cs.york.ac.uk/,frisch/papers/mi16.ps. [13] A.M. Frisch and T.J. Peugniez, Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings, 1999. Available at http://www.cs.york.ac.uk/,frisch/papers/nbwalksat.ps. [14] D. Frost and R. Dechter. Dead-end driven learning. In Proceedings of the 12th National Conference on AI, pages 301-306. American Association for Artificial Intelligence, 1994. [15] D. Frost and R. Dechter. Optimizing with constraints: a case study in scheduling maintenance of electric power units. In Proceedings of the 5th International Symposium on Artificial Intelligence and Mathematics, 1998. To appear in the Annals of Mathematics and AI. [16] I.P. Gent, E. MacIntyre, P. Prosser, P. Shaw, and T. Walsh. The constrainedness of arc consistency. In 3rd International Conference on Principles and Practices of Constraint Programming (CP-97), pages 327-340. Springer, 1997. [17] I.P. Gent, E. MacIntyre, P. Prosser, B.M. Smith, and T. Walsh. An empirical study of dynamic variable ordering heuristics for the constraint satisfaction problem. In 2nd International Conference on Principles and Practices of Constraint Programming (CP-96), pages 179-193, 1996. [18] I.P. Gent, E. MacIntyre, P. Prosser, and T. Walsh. Scaling effects in the CSP phase transition. In 1st International Conference on Principles and Practices of Constraint Programming (CP-95), pages 70-87. Springer-Verlag, 1995. [19] I.P. Gent, E. MacIntyre, P. Prosser, and T. Walsh. The constrainedness of search. In Proceedings of the 13th National Conference on AI, pages 246-252. American Association for Artificial Intelligence, 1996. [20] I.P. Gent and T. Walsh. An empirical analysis of search in GSAT. Journal of Artificial Intelligence Research, 1:23-57, 1993. [21] I.P. Gent and T. Walsh. Towards an Understanding of Hill-climbing Procedures for SAT. In Proceedings of the 11th National Conference on AI. American Association for Artificial Intelligence, 1993. [22] I.P. Gent and T. Walsh. The SAT phase transition. In A G Cohn, editor, Proceedings of 11th ECAI, pages 105-109. John Wiley & Sons, 1994. [23] I.P. Gent and T. Walsh. The satisfiability constraint gap. Artificial Intelligence, 81(1-2), 1996. [24] J.N. Hooker. Constraint satisfaction methods for generating valid cuts. In D. L. Woodruf, editor, Advances in Computational and Stochastic Optimization, Logic Programming, and Heuristic Search, pages 1-30. Kluwer, 1997. [25] E. MacIntyre, P. Prosser, B.M. Smith, and T. Walsh. Random constraint satisfaction: Theory meets practice. In 4th International Conference on Principles and Practices of Constraint Programming (CP-98), pages 325-339. Springer, 1998. [26] J-C. R'egin. A filtering algorithm for constraints of difference in CSPs. In Proceedings of the 12th National Conference on AI, pages 362-367. American Association for Artificial Intelligence, 1994. [27] A. Robinson. A Machine oriented Logic Based on the resolution principle. Journal of the ACM, 12:23-41, 1965. [28] B.M. Smith, K. Stergiou, and T. Walsh. Modelling the Golomb ruler problem. In Proceedings of the IJCAI 99 Workshop on Non-Binary Constraints. International Joint Conference on Artificial Intelligence, 1999. Also available as APES report, APES-11-1999 from http://apes.cs.strath.ac.uk/reports/apes-11-1999.ps.gz. [29] K. Stergiou and T. Walsh. The difference all-difference makes. In Proceedings of 16th IJCAI. International Joint Conference on Artificial Intelligence, 1999. [30] K. Stergiou and T. Walsh. Encodings of non-binary constraint satisfaction problems. In Proceedings of the 16th National Conference on AI. American Association for Artificial Intelligence, 1999. [31] T. Walsh. A divergence critic for inductive proof. Journal of Artificial Intelligence Research, 4:209-235, 1996. [32] T. Walsh. Depth-bounded discrepancy search. In Proceedings of 15th IJCAI, pages 1388-1387. International Joint Conference on Artificial Intelligence, 1997.