Using More Reasoning To Improve #SAT Solving
Jessica Davies and Fahiem Bacchus

Abstract

Many real-world problems, including inference in Bayes Nets, can be reduced to #SAT, the problem of counting the number of models of a propositional theory. This has motivated the need for efficient #SAT solvers. Currently, such solvers utilize a modified version of DPLL that employs decomposition and caching, techniques that significantly increase the time it takes to process each node in the search space. In addition, the search space is significantly larger than when solving SAT since we must continue searching even after the first solution has been found. It has previously been demonstrated that the size of a DPLL search tree can be significantly reduced by doing more reasoning at each node. However, for SAT the reductions gained are often not worth the extra time required. In this paper we verify the hypothesis that for #SAT this balance changes. In particular, we show that additional reasoning can reduce the size of a #SAT solvers search space, that this reduction cannot always be achieved by the already utilized technique of clause learning, and that this additional reasoning can be cost effective.

A Situation-Calculus Semantics for an Expressive Fragment of PDDL
by Yuxiao Hu

Abstract

The Planning Domain Definition Language (PDDL) has become a common language to specify planning problems, facilitating the formulation of benchmarks and a direction comparison of planners. Over the years PDDL has been extended beyond STRIPS and ADL in various directions, for example, by adding time and concurrent actions. The current semantics of PDDL is purely meta-theoretic and quite complex, which makes an analysis difficult. Moreover, relating the language to other action formalisms is also nontrivial. We propose an alternative semantics for an expressive fragment of PDDL within the situation calculus. This yields at least two advantages. For one, the new semantics is purely declarative, making it amenable to an analysis in terms of logical entailments. For another, it facilitates the comparison with and mapping to other formalisms that are defined on top of the same logic, such as the agent control language Golog. In particular we obtain the semantical foundation for embedding efficient PDDL-based planners into the more expressive, yet computationally expensive Golog, thus combining the benefits of both. Other by-products of our investigations are a simpler account of durative actions in the situation calculus and a new notion of compulsory actions.

Using Expectation Maximization to Find Likely Assignments for Constraint Satisfaction Problems
by Eric Hsu, Matthew Kitching, Fahiem Bacchus, Sheila McIlraith
(Speaker: Eric Hsu)

A Logical Theory of Coordination and Joint Ability
by Hojjat Ghaderi

Using Expectation Maximization to Find Likely Assignments for Constraint Satisfaction Problems
by Eric Hsu, Matthew Kitching, Fahiem Bacchus, Sheila McIlraith
Abstract:
We present a new probabilistic framework for finding likely variable assignments in difficult constraint satisfaction problems. Finding such assignments is key to efficient search, but practical efforts have largely been limited to random guessing and heuristically designed weighting systems. In constrast, we derive a new version of Belief Propagation (BP) using the method of Expectation Maximization (EM). This allows us to differentiate between variables that are strongly biased toward particular values and those that are essentially extraneous. Using EM also eliminates the threat of nonconvergence associated with regular BP. Theoretically, the derivation exhibits appealing primal/dual semantics. Empirically, it produces an EMBP-based heuristic that outperforms existing techniques for guiding variable and value ordering during backtracking search.

A Logical Theory of Coordination and Joint Ability
by Hojjat Ghaderi
Abstract:
A team of agents is jointly able to achieve a goal if despite any incomplete knowledge they may have about the world or each other, they still know enough to be able to get to a goal state. Unlike in the single-agent case, the mere existence of a working plan is not enough as there may be several incompatible working plans and the agents may not beable to choose a share that coordinates with those of the others. Some formalizations of joint ability ignore this issue of coordination within a coalition. Others, including those based on game theory, deal with coordination, but require a complete specification of what the agents believe. Such a complete specification is often not available. Here we present a new formalization of joint ability based on logical entailment in the situation calculus that avoids both of these pitfalls.

In this talk I will present our current results about efficient logical filtering algorithms and complexity bounds. Logical filtering is hard in general, so I will focus on three types of propositional systems for which polynomial time filtering is possible (the first two also enable polynomial time inquiry):
(1) Systems in which actions are variants of STRIPS, i.e., non-deterministic systems with no conditional effects.
(2) Systems in which actions can be characterized with non-singular Boolean matrices, and
(3) Deterministic actions of few effects and preconditions.
I will give the main ideas behind tractability of these systems and also behind intractability of the general case.

Our results affect future investigations into monitoring, planning, diagnosis, real-time control, and reinforcement learning in partially observable domains. They have already been applied to learning and planning in partially observable domains. They also lead to more efficient stochastic filtering.

This talk includes materials from [Amir & Russell; IJCAI ‘03], [Shahaf & Amir; IJCAI ‘07], [Amir & Russell; J. manuscript in preparation]

Applications mentioned in this talk appear in [Amir; IJCAI ‘05], [Shahaf & Amir; AAAI ‘06], [Shahaf etal.; AAAI ‘06], [Chang & Amir; ICAPS’06]

URL: http://reason.cs.uiuc.edu/eyal

Classen et al recently defined a declarative semantics for the ADL subset of PDDL. We extend their result to include the temporal features in PDDL 2.x, such as durative actions and concurrency, among other things. Unlike the existing state-transitional semantics which is complex and purely meta-theoretic, our definition is based on logical theories in ES, a variant of the situation calculus. This result makes it possible to analyze temporal planning problems in terms of logical entailments, and facilitates the unification between planning and other formalisms, like the action language Golog.

A team of agents is jointly able to achieve a goal if despite any incomplete knowledge they may have about the world or each other, they still know enough to be able to get to a goal state.Unlike in the single-agent case, the mere existence of a working plan is not enough as there may be several incompatible working plans and the agents may not be able to choose a share that coordinates with the others’. Some formalizations of joint ability ignore this issue of coordination within a coalition. Others, including those based on game theory, deal with coordination, but require a complete specification of agents’ beliefs. Such a complete specification is often not available. Here we present a new formalization of joint ability based on logical entailment in the situation calculus that avoids both of these pitfalls.

Paper:
http://www.ucl.ac.uk/commonsense07/papers/ghaderi-levesque-lesperance.pdf

Abstract

The action language Golog has been applied successfully to the control of robots, among other things. Perhaps the greatest advantage of the language is that a user can write programs which constrain the search for an executable plan in a flexible manner. However, when general planning is needed, Golog supports this only in principle, but does not measure up with state-of-the-art planners. In this paper we propose an integration of Golog and planning in the sense that planning problems, formulated as part of a Golog program, are solved by a modern planner during the execution of the program. Here we focus on the ADL subset of the plan language PDDL. First we show that the semantics of ADL can be understood as progression in the situation calculus, which underlies Golog, thus providing us with a correct embedding of ADL within Golog. We then show how Golog can be integrated with an existing ADL planner for closed-world initial databases and compare the performance of the resulting system with the original Golog.

Abstract

Checkers for propositional satisfiability (SAT solvers) are the most effective tools for solving important classes of industrial-scale problems (in computer-aided design of integrated circuits, planning, model checking, scheduling, cryptography, …). One step “ahead” of SAT solvers, we encounter QBF provers. They manipulate the language of QBFs (Quantified Boolean Formulas), which adds the valuable possibility of quantifying universally over the truth value of variables. Such extra capability allows us to capture further application-relevant problems, and to obtain substantially compressed representations for classical ones (e.g. bounded model checking). Unquestionably, the most effective complete method to decide SAT is backtracking search (the “DPLL” method). The same was true of QBF, until 2004. Since then, several alternative decision procedures have been proposed which seem to tarnish the unrivaled reputation of the “search paradigm” in propositional reasoning. When universal quantifiers enter the game, alternative forms of reasoning which are more abstract than brute search gain credibility. In this seminar, we discuss the algorithms and techniques employed by a state-of-the-art QBF solver (sKizzo) which does its best to eschew “search”. Among these techniques we mention: quantifier elimination, symbolic skolemization, and abstract branching. Experimental results and applications to real-world cases are also discussed, together with the issues in certifying the correctness of solvers’ answers.

Speaker’s Biography

After obtaining his PhD in 2002 at DIS (Department of Informatics and Systems Science, Univ. La Sapienza, Rome, Italy) with a thesis entitled “Bridging Refutation and Search in Propositional Satisfiability”, Marco Benedetti moved to ITC-Irst (Institute for Scientific and Technological Research, Trento, Italy) where he has been working on SAT-based techniques for Model Checking. In the last few years he has focused on the theory and applications of Quantified Boolean Formulas (QBFs), a framework that allows to automate eduction in formal verification, planning, model checking, etc. He has developed many algorithms and techniques for evaluating and certifying QB formulas, all of which are implemented in the state-of-the-art solver “sKizzo”. Currently, Dr. Benedetti is a Research Associate at LIFO (Laboratoire d’Informatique Fondamentale d’Orléans, France), where he works mainly on extensions of Quantified Constraint Satisfaction Problems (QCSPs), for which he has co-designed a publicly available solver called QeCode.

Abstract:

In this talk I present two approaches for knowledge assimilation from
vision data: the first includes a novel logic-based formalism for
representing knowledge about objects in space and their movements
(including the observer). In this framework space is represented using
functions that extract attributes of depth, size and distance from
snapshots of the world. The second part of the talk presents a cognitive
vision system capable of autonomously learning protocols from perceptual
observations of dynamic scenes. These approaches are motivated by the aim
of creating a synthetic agent that can interpret scenes containing
interactions between unknown objects and agents, and learn models of these
that are sufficient to allow the agent to act in accordance with the
implicit protocols present in the scenes.

Paulo E. Santos, Ph.D.
Dept. of Electrical and Electronics Engineering
Centro Universitario da Fei
Sao Paulo, Brazil
http://www.fei.edu.br/~psantos/