1,720,964 research outputs found
On compact representations of propositional circumscription
We prove that -.unless the polynomial hierarchy collapses at the second level - the size of a purely propositional representation of the circumscription CIRC(T) of a propositional formula T grows faster than any polynomial as the size of T increases. We then analyze the significance of this result in the related field of closed-world reasoning
Approximate entailment
Approximation techniques are widely used in many areas of Computer Science for dealing with polynomially intractable problems. The major difficulty about introducing approximation in reasoning problems is in that it is very hard to find a measure of the approximation which is not dependent on the particular problem at hand. Our goal is to introduce the notion of approximate answers to reasoning problems which are known to be computationally intractable. We focus our attention on a reasoning problem which is both very general and computationally intractable: checking whether a propositional formula in Conjunctive Normal Form entails a clause. We present two sequences of entailment relations approximating the classical one: the relations of the first sequence are sound but not complete, while the relations of the second one are complete but not sound. Both sequences converge to classical entailment and can be computed in polynomial time under some conditions. Our claim is that both these sequences are an approximation of the entailment relation, since they always provide information clearly related to the original problem. In the last part of the paper, we sketch an algorithm for computing incrementally relations of the two sequence
FONDAMENTI DELLA PROGETTAZIONE DEI PROGRAMMI. PRINCIPI, TECNICHE E LORO APPLICAZIONI IN C++
Compiling problem specifications into SAT
Springer-Verlag Lecture Notes in Computer Scienc
Compiling problem specifications into SAT
We present a compiler that translates a problem specification into a propositional satisfiability
test (SAT). Problems are specified in a logic-based language, called NP-SPEC, which allows the
definition of complex problems in a highly declarative way, and whose expressive power is such as
to capture all problems which belong to the complexity class NP. The target SAT instance is solved
using any of the various state-of-the-art solvers available from the community. The system obtained
is an executable specification language for all NP problems which shows interesting computational
properties. The performance of the system has been tested on a few classical problems, namely
graph coloring, Hamiltonian cycle, job-shop scheduling, and on a real-world scheduling application,
namely the tournament scheduling problem
Going Beyond Counting First Authors in Author Co-citation Analysis
The present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae
. Although Knowledge Representation is full of reasoning problems that have been formally proved to be both NP-hard and coNP-hard, the experimental analysis has largely focused on problems belonging to either NP or coNP. We still do not know, for example, whether wellstudied phenomena such as "phase transition", which show up for many NP-complete problems (e.g., sat) happen for \Sigma p 2 -complete problems, and whether they are related to an "easy-hard-easy" pattern or not. The goal of this paper is to show some results of an ongoing experimental analysis that aims to provide reasonable answers to such questions. We analyze the problem of evaluating Quantified Boolean Formulae, which is the prototypical complete problem for all levels of the Polynomial Hierarchy, the computationally simplest hierarchy of complexity classes above NP of great interest to KR. Appearing on the Proceedings of the 5th Congress of the Italian Association for Artificial Intelligence (AI*IA'97) September 16..
- …
