Constraint-Based Reasoning
A Unified Framework for Planning and Execution-Monitoring of Mobile Robots
Gianni, Mario (University of Rome "La Sapienza) | Papadakis, Panagiotis (University of Rome "La Sapienza) | Pirri, Fiora (University of Rome "La Sapienza") | Liu, Ming (Swiss Federal Institute of Technology,) | Pomerleau, Francois (Swiss Federal Institute of Technology,) | Colas, Francis (Swiss Federal Institute of Technology, Zurich) | Zimmermann, Karel (Czech Technical University, Prague) | Svoboda, Tomas (Czech Technical University, Prague) | Petricek, Tomas (Czech Technical University, Prague) | Kruijff, Geert (German Research Center for Artificial Intelligence) | Khambhaita, Harmish (German Research Center for Artificial Intelligence) | Zender, Hendrik (German Research Center for Artificial Intelligence)
We present an original integration of high level planning and execution with incoming perceptual information from vision, SLAM, topological map segmentation and dialogue. The task of the robot system, implementing the integrated model, is to explore unknown areas and report detected objects to an operator, by speaking loudly. The knowledge base of the planner maintains a graph-based representation of the metric map that is dynamically constructed via an unsupervised topological segmentation method, and augmented with information about the type and position of detected objects, within the map, such as cars or containers. According to this knowledge the cognitive robot can infer strategies in so generating parametric plans that are instantiated from the perceptual processes. Finally, a model-based approach for the execution and control of the robot system is proposed to monitor, concurrently, the low level status of the system and the execution of the activities, in order to achieve the goal, instructed by the operator.
Continual Planning with Sensing for Web Service Composition
Kaldeli, Eirini (University of Groningen) | Lazovik, Alexander (University of Groningen) | Aiello, Marco (University of Groningen)
Web Service (WS) domains constitute an application field where automated planning can significantly contribute towards achieving customisable and adaptable compositions. Following the vision of using domain-independent planning and declarative complex goals to generate compositions based on atomic service descriptions, we apply a planning framework based on Constraint Satisfaction techniques to a domain consisting of WSs with diverse functionalities. One of the key requirements of such domains is the ability to address the incomplete knowledge problem, as well as recovering from failures that may occur during execution. We propose an algorithm for interleaving planning, monitoring and execution, where continual planning via altering the CSP is performed, under the light of the feedback acquired at runtime. The system is evaluated against a number of scenarios including real WSs, demonstrating the leverage of situations that can be effectively tackled with respect to previous approaches.
Hybrid Tractable Classes of Binary Quantified Constraint Satisfaction Problems
Gao, Jian (Northeast Normal University) | Yin, Minghao (Northeast Normal University) | Zhou, Junping (Northeast Normal University)
In this paper, we investigate the hybrid tractability of binary Quantified Constraint Satisfaction Problems (QCSPs). First, a basic tractable class of binary QCSPs is identified by using the broken-triangle property. In this class, the variable ordering for the broken-triangle property must be same as that in the prefix of the QCSP. Second, we break this restriction to allow that existentially quantified variables can be shifted within or out of their blocks, and thus identify some novel tractable classes by introducing the broken-angle property. Finally, we identify a more generalized tractable class, i.e., the min-of-max extendable class for QCSPs.
Symmetric Graph Regularized Constraint Propagation
Fu, Zhenyong (City University of Hong Kong) | Lu, Zhiwu (Peking University) | Ip, Horace (City University of Hong Kong) | Peng, Yuxin (Peking University) | Lu, Hongtao (Shanghai Jiao Tong University)
This paper presents a novel symmetric graph regularization framework for pairwise constraint propagation. We first decompose the challenging problem of pairwise constraint propagation into a series of two-class label propagation subproblems and then deal with these subproblems by quadratic optimization with symmetric graph regularization. More importantly, we clearly show that pairwise constraint propagation is actually equivalent to solving a Lyapunov matrix equation, which is widely used in Control Theory as a standard continuous-time equation. Different from most previous constraint propagation methods that suffer from severe limitations, our method can directly be applied to multi-class problem and also can effectively exploit both must-link and cannot-link constraints. The propagated constraints are further used to adjust the similarity between data points so that they can be incorporated into subsequent clustering. The proposed method has been tested in clustering tasks on six real-life data sets and then shown to achieve significant improvements with respect to the state of the arts.
Adaptive Neighborhood Inverse Consistency as Lookahead for Non-Binary CSPs
Woodward, Robert J. (University of Nebraska-Lincoln) | Karakashian, Shant (University of Nebraska-Lincoln) | Choueiry, Berthe Y. (University of Nebraska-Lincoln) | Bessiere, Christian (University of Montpellier)
Freuder and Elfe (1996) introduced Neighborhood Inverse Consistency (NIC) for binary CSPs. In this paper, we introduce RNIC, the extension of NIC to non-binary CSPs, and describe a practical algorithm for enforcing it. We propose an adaptive strategy to weaken or strengthen this property based on the connectivity of the network. We demonstrate the effectiveness of RNIC as a full lookahead strategy during search for solving difficult benchmark problems.
On Expressing Value Externalities in Position Auctions
Constantin, Florin (Georgia Institute of Technology) | Rao, Malvika (Harvard University) | Huang, Chien-Chung (Humboldt-Universität zu Berlin) | Parkes, David (Harvard University)
We introduce a bidding language for expressing negative value externalities in position auctions for online advertising. The unit-bidder constraints (UBC) language allows a bidder to condition a bid on its allocated slot and on the slots allocated to other bidders. We introduce a natural extension of the Generalized Second Price (GSP) auction, the expressive GSP (eGSP) auction, that induces truthful revelation of constraints for a rich subclass of unit-bidder types, namely downward-monotonic UBC. We establish the existence of envy-free Nash equilibrium in eGSP under a further restriction to a subclass of exclusion constraints, for which the standard GSP has no pure strategy Nash equilibrium. The equilibrium results are obtained by reduction to equilibrium analysis for reserve price GSP (Even-Dar et al. 2008). In considering the winner determination problem, which is NP-hard, we bound the approximation ratio for social welfare in eGSP and provide parameterized complexity results.
Exact Phase Transitions and Approximate Algorithm of #CSP
Huang, Ping (Northeast Normal University) | Yin, Minghao (Northeast Normal University) | Xu, Ke (Beijing University of Aeronautics and Astronautics)
The study of phase transition phenomenon of NP complete problems plays an important role in understanding the nature of hard problems. In this paper, we follow this line of research by considering the problem of counting solutions of Constraint Satisfaction Problems (#CSP). We consider the random model, i.e. RB model. We prove that phase transition of #CSP does exist as the number of variables approaches infinity and the critical values where phase transitions occur are precisely located. Preliminary experimental results also show that the critical point coincides with the theoretical derivation. Moreover, we propose an approximate algorithm to estimate the expectation value of the solutions number of a given CSP instance of RB model.
Limits of Preprocessing
Szeider, Stefan (Vienna University of Technology)
We present a first theoretical analysis of the power of polynomial-time preprocessing for important combinatorial problems from various areas in AI. We consider problems from Constraint Satisfaction, Global Constraints, Satisfiability, Nonmonotonic and Bayesian Reasoning. We show that, subject to a complexity theoretic assumption, none of the considered problems can be reduced by polynomial-time preprocessing to a problem kernel whose size is polynomial in a structural problem parameter of the input, such as induced width or backdoor size. Our results provide a firm theoretical boundary for the performance of polynomial-time preprocessing algorithms for the considered problems.
A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT
Jain, Siddhartha (Brown University) | Sabharwal, Ashish (IBM T. J. Watson Research Center) | Sellmann, Meinolf (IBM T. J. Watson Research Center)
We formulate a general framework for pseudo-Boolean multi-valued nogood-learning, generalizing conflict analysis performed by modern SAT solvers and its recent extension for disjunctions of multi-valued variables. This framework can handle more general constraints as well as different domain representations, such as interval domains which are commonly used for bounds consistency in constraint programming (CP), and even set variables. Our empirical evaluation shows that our solver, built upon this framework, works robustly across a number of challenging domains.
Core-Guided Binary Search Algorithms for Maximum Satisfiability
Heras, Federico (University College Dublin) | Morgado, Antonio (University College Dublin) | Marques-Silva, Joao (University College Dublin)
Several MaxSAT algorithms based on iterative SAT solving have been proposed in recent years. These algorithms are in general the most efficient for real-world applications. Existing data indicates that, among MaxSAT algorithms based on iterative SAT solving, the most efficient ones are core-guided, i.e. algorithms which guide the search by iteratively computing unsatisfiable subformulas (or cores). For weighted MaxSAT, core-guided algorithms exhibit a number of important drawbacks, including a possibly exponential number of iterations and the use of a large number of auxiliary variables. This paper develops two new algorithms for (weighted) MaxSAT that address these two drawbacks. The first MaxSAT algorithm implements core-guided iterative SAT solving with binary search. The second algorithm extends the first one by exploiting disjoint cores. The empirical evaluation shows that core-guided binary search is competitive with current MaxSAT solvers.