Marco Schaerf

SAT Conference 2011 Conference Paper

Applying UCT to Boolean Satisfiability

• Alessandro Previti
• Raghuram Ramanujan
• Marco Schaerf
• Bart Selman

Abstract In this paper we perform a preliminary investigation into the application of sampling-based search algorithms to satisfiability testing of propositional formulas in Conjunctive Normal Form (CNF). In particular, we adapt the Upper Confidence bounds applied to Trees (UCT) algorithm [5] which has been successfully used in many game playing programs including MoGo, one of the strongest computer Go players [3].

I&C Journal 2002 Journal Article

Preprocessing of Intractable Problems

• Marco Cadoli
• Francesco M. Donini
• Paolo Liberatore
• Marco Schaerf

Some computationally hard problems, e. g. , deduction in logical knowledge bases– are such that part of an instance is known well before the rest of it, and remains the same for several subsequent instances of the problem. In these cases, it is useful to preprocess off-line this known part so as to simplify the remaining on-line problem. In this paper we investigate such a technique in the context of intractable, i. e. , NP-hard, problems. Recent results in the literature show that not all NP-hard problems behave in the same way: for some of them preprocessing yields polynomial-time on-line simplified problems (we call them compilable), while for other ones their compilability implies some consequences that are considered unlikely. Our primary goal is to provide a sound methodology that can be used to either prove or disprove that a problem is compilable. To this end, we define new models of computation, complexity classes, and reductions. We find complete problems for such classes, “completeness” meaning they are “the less likely to be compilable. ” We also investigate preprocessing that does not yield polynomial-time on-line algorithms, but generically “decreases” complexity. This leads us to define “hierarchies of compilability, ” that are the analog of the polynomial hierarchy. A detailed comparison of our framework to the idea of “parameterized tractability” shows the differences between the two approaches.

KR Conference 2002 Conference Paper

Solving QBF by SMV

• Francesco M. Donini
• Paolo Liberatore
• Fabio O. P. Massacci
• Marco Schaerf

AIJ Journal 1999 Journal Article

The size of a revised knowledge base

• Marco Cadoli
• Francesco M. Donini
• Paolo Liberatore
• Marco Schaerf

In this paper we address a specific computational aspect of belief revision: the size of the propositional formula obtained by means of the revision of a formula with a new one. In particular, we focus on the size of the smallest formula which is logically equivalent to the revised knowledge base. The main result of this paper is that not all formalizations of belief revision are equal from this point of view. For some of them we show that the revised knowledge base can be represented by a polynomial-size formula (we call these results “compactability” results). On the other hand, for other ones the revised knowledge base does not always admit a polynomial-space representation, unless the polynomial hierarchy collapses at a sufficiently low level (“non-compactability” results). We also show that the time complexity of query answering for the revised knowledge base has definitely an impact on being able to represent the result of the revision compactly. Nevertheless, formalisms with the same complexity may have different compactability properties. We also study compactability properties for a weaker form of equivalence, called query equivalence, which allows to introduce new propositional symbols. Moreover, we extend our analysis to the special case in which the new formula has constant size and to the case of sequences of revisions (i. e. , iterated belief revision). A complete analysis along these four coordinates is shown.

ECAI Conference 1998 Conference Paper

The Complexity of Model Checking for Propositional Default Logics

• Paolo Liberatore
• Marco Schaerf

TCS Journal 1997 Journal Article

On compact representations of propositional circumscription

• Marco Cadoli
• Francesco M. Donini
• Marco Schaerf
• Riccardo Silvestri

Circumscription is a popular common-sense reasoning technique, used in the fields of Artificial Intelligence, Databases and Logic Programming. In this paper we investigate the size of representations (formulae, data structures) equivalent to the circumscription of a propositional formula T, taking into account three different definitions of equivalence. We find necessary and sufficient conditions for the existence of polynomial-size representations (formulae, data structures) equivalent to the circumscription of T in the three cases. All such conditions imply the collapse of the polynomial hierarchy. In particular, we prove that — unless the polynomial hierarchy collapses at the second level — the size of the shortest propositional formula T′ logically equivalent to the circumscription of T grows faster than any polynomial as the size of T increases. The significance of this result in the related field of closed-world reasoning is then analyzed.

AIJ Journal 1997 Journal Article

Reducing belief revision to circumscription (and vice versa)

• Paolo Liberatore
• Marco Schaerf

Nonmonotonic formalisms and belief revision operators have been introduced as useful tools to describe and reason about evolving scenarios. Both approaches have been proven effective in a number of different situations. However, little is known about their relationship. Previous work by Winslett has shown some correlations between a specific operator and circumscription. In this paper we greatly extend Winslett's work by establishing new relations between circumscription and a large number of belief revision operators. This highlights similarities and differences between these formalisms. Furthermore, these connections provide us with the possibility of importing results in one field into the other one.

AIJ Journal 1996 Journal Article

Is intractability of nonmonotonic reasoning a real drawback?

• Marco Cadoli
• Francesco M. Donini
• Marco Schaerf

Several studies about computational complexity of nonmonotonic reasoning (NMR) showed that nonmonotonic inference is significantly harder than classical, monotonic inference. This contrasts with the general idea that NMR can be used to make knowledge representation and reasoning simpler, not harder. In this paper we show that, to some extent, NMR fulfills the representation goal. In particular, we prove that nonmonotonic formalisms such as circumscription and default logic allow for a much more compact and natural representation of propositional knowledge than propositional calculus. Proofs are based on a suitable definition of a compilable inference problem, and on non-uniform complexity classes. Some results about intractability of circumscription and default logic can therefore be interpreted as the price one has to pay for having such an extra-compact representation. On the other hand, intractability of inference and compactness of representation are not equivalent notions: we exhibit intractable nonmonotonic formalisms whose nonmonotonic assumptions are representable by few propositional formulae. Finally, sometimes NMR really makes reasoning simpler. We present prototypical scenarios where closed-world reasoning and well-founded semantics account for a faster, complete and unsound approximation of classical reasoning.

AIJ Journal 1995 Journal Article

Tractable reasoning via approximation

• Marco Schaerf
• Marco Cadoli

Problems in logic are well known to be hard to solve in the worst case. Two different strategies for dealing with this aspect are known from the literature: language restriction and theory approximation. In this paper we are concerned with the second strategy. Our main goal is to define a semantically well-founded logic for approximate reasoning, which is justifiable from the intuitive point of view, and to provide fast algorithms for dealing with it even when using expressive languages. We also want our logic to be useful to perform approximate reasoning in different contexts. We define a method for the approximation of decision reasoning problems based on multivalued logics. Our work expands and generalizes, in several directions, ideas presented by other researchers. The major features of our technique are: (1) approximate answers give semantically clear information about the problem at hand; (2) approximate answers are easier to compute than answers to the original problem; (3) approximate answers can be improved, and eventually they converge to the right answer; (4) both sound approximations and complete ones are described. The method we propose is flexible enough to be applied to a wide range of reasoning problems. In our research we considered approximation of several decidable problems with different worstcase complexity, involving both propositional and first-order languages. In particular we defined approximation techniques for: propositional logic, fragments of first-order logic (concept description languages) and modal logic. In our research we also addressed the issue of representing the knowledge of a reasoner with limited resources and how to use such a knowledge for approximate reasoning purposes.

ECAI Conference 1992 Conference Paper

Approximate Inference in Default Logic and Circumscription

• Marco Cadoli
• Marco Schaerf

TARK Conference 1992 Conference Paper

Approximate Reasoning and Non-Omniscient Agents

• Marco Cadoli
• Marco Schaerf

Modal logics have been frequently used to represent the knowledge and belief owned by an agent. However, such systems make the unrealistic assumption that agents are logically omniscent, hence capable of performing extremely complex inferences. Our goal in this paper is twofold. First of all we show that an approximation pattern can be used for a stepwise procedure which determines the satisfiability of a formula in several modal systems like 85, ~, 2r and 84. This method is based on a generalization of the standard possible-world semantics for modal logic. Secondly, we use this semantics to define a modal language which allows the explicit representation of the knowledge owned by a resource-limited agent.