| |
|
| |
|
| |
Abstract
We give an overview of interactive methods developed for solving nonlinear multiobjective optimization problems. In interactive methods, a decision maker plays an important part and the idea is to support her/him in the search for the most preferred solution. In interactive methods, steps of an iterative solution algorithm are repeated and the decision maker progressively provides preference information so that the most preferred solution can be found. We identify three types of specifying preference information in interactive methods and give some ...
|
| |
Abstract
We study the runtime distributions of backtrack procedures for propositional satisfiability and constraint satisfaction. Such procedures often exhibit a large variability in performance. Our study reveals some intriguing properties of such distributions: They are often characterized by very long tails or “heavy tails”. We will show that these distributions are best characterized by a general class of distributions that can have infinite moments (i.e., an infinite mean, variance, etc.). Such nonstandard distributions have recently been observed in areas as diverse as ...
|
| |
(2011)
Abstract
* Contains additional discussion and examples on left truncation as well as material on more general censoring and truncation patterns. * Introduces the martingale and counting process formulation swil lbe in a new chapter. * Develops multivariate failure time data in a separate chapter and extends the material on Markov and semi Markov formulations. * Presents new examples and applications of data analysis. ...
|
| |
Abstract
Determining whether a propositional theory is satisfiable is a prototypical example of an NP-complete problem. Further, a large number of problems that occur in knowledge-representation, learning, planning, and other areas of AI are essentially satisfiability problems. This paper reports on the most extensive set of experiments to date on the location and nature of the crossover point in satisfiability problems. These experiments generally confirm previous results with two notable exceptions. First, we have found that neither of the functions previously proposed ...
|
| |
In 15th International Conference on Theory and Applications of Satisfiability Testing (SAT) (2005)
|
| |
Journal on Satisfiability, Boolean Modeling and Computation (JSAT) (2010)
|
| |
Journal of Statistical Software (2008)
posted to seriation software
by bsilverthorn
on 2012-03-06 22:47:55
|
| |
Abstract
In this paper we generalize a heuristic that we have introduced previously for solving efficiently random 3-SAT formulae. Our heuristic is based on the notion of backbone, searching variables belonging to local backbones of a formula. This heuristic was limited to 3-SAT formulae. In this paper we generalize this heuristic by introducing a sub-heuristic called a re-normalization heuristic in order to handle formulae with various clause lengths and particularly hard random k - sat formulae with k ≥ 3 . We ...
|
| |
Abstract
The goal of this paper is to test if a programming methodology based on the declarative language A-Prolog and the systems for computing answer sets of such programs, can be successfully applied to the development of medium size knowledge-intensive applications. We report on a successful design and development of such a system controlling some of the functions of the Space Shuttle. ...
|
| |
Abstract
Michael Gelfond’s application of Answer Set Programming (ASP) in the context of NASA’s space shuttle has opened the door of the ivory tower. His project has not only given our community self-confidence and served us as a reference for grant agencies and neighboring fields, but ultimately it helped freeing the penguins making them exclaim “Yes, we can [fly] !” . The community has taken up this wonderful assist to establish ASP as a prime tool for declarative problem solving in the ...
|
| |
In Proceedings of the 26th International Conference on Machine Learning (ICML) (2010)
Abstract
Identifying the most influential documents in a corpus is an important problem in many fields, from information science and historiography to text summarization and news aggregation. Unfortunately, traditional bibliometrics such as citations are often not available. We propose using changes in the thematic content of documents over time to measure the importance of individual documents within the collection. We describe a dynamic topic model for both quantifying and qualifying the impact of these documents. We validate the model by analyzing three ...
|
| |
In Proceedings of the 28th International Conference on Machine Learning (ICML) (2011)
|
| |
posted to constraint_satisfaction
by bsilverthorn
on 2012-03-01 19:28:57
Abstract
The order in which the variables are assigned can have an enormous impact on the time taken by a backtracking search algorithm to solve a constraint satisfaction problem (CSP). The Brélaz heuristic is a dynamic variable ordering heuristic which has been shown to give good results for some classes of binary CSPs when the constraint graph is not complete. Its advantage over the simpler smallest-domain heuristic is that it uses information about the constraint graph. This paper uses theoretical work by ...
|
| |
In Proceedings of the 6th International Conference on Learning and Intelligent Optimization (LION) (2012)
posted to algorithm_configuration
by bsilverthorn
on 2012-02-29 17:44:31
|
| |
|
| |
In Proceedings of the 20th International Joint Conference on Artifical Intelligence (IJCAI) (2007)
posted to sat_solvers
by bsilverthorn
on 2012-02-29 03:24:28
Abstract
Given the common use of restarts in today's clause learning SAT solvers, the task of choosing a good restart policy appears to have attracted remarkably little interest. On the other hand, results have been reported on the use of different restart policies for combinatorial search algorithms. Such results are not directly applicable to clause learning SAT solvers, as the latter are now understood as performing a form of resolution, something fundamentally different from search (in the sense of backtracking search for ...
|
| |
In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI) (2010)
posted to algorithm_configuration
by bsilverthorn
on 2012-02-29 02:58:17
Abstract
We present a new method for instance-specific algorithm configuration (ISAC). It is based on the integration of the algorithm configuration system GGA and the recently proposed stochastic offline programming paradigm. ISAC is provided a solver with categorical, ordinal, and/or continuous parameters, a training benchmark set of input instances for that solver, and an algorithm that computes a feature vector that characterizes any given instance. ISAC then provides high quality parameter settings for any new input instance. Experiments on a variety of ...
|
| |
posted to parameter_adjustment
by bsilverthorn
on 2012-02-29 02:46:58
Abstract
Instance-Specific Algorithm Configuration (ISAC) is a novel general technique for automatically generating and tuning algorithm portfolios. The approach has been very successful in practice, but up to now it has been committed to using all the features it was provided. However, traditional feature filtering techniques are not applicable, requiring multiple computationally expensive tuning steps during the evaluation stage. To this end, we show three new evaluation functions that use precomputed runtimes of a collection of untuned solvers to quickly evaluate subsets ...
|
| |
In Proceedings of the 23rd Benelux Conference on Artificial Intelligence (2011)
|
| |
(2010)
posted to empirical_hardness
by bsilverthorn
on 2012-02-29 02:25:34
|
| |
Abstract
In this paper we study the problem of yielding robust performances from current state-of-the-art solvers for quantified Boolean formulas (QBFs). Building on top of existing QBF solvers, we implement a new multi-engine solver which can inductively learn its solver selection strategy. Experimental results confirm that our solver is always more robust than each single engine, that it is stable with respect to various perturbations, and that such results can be partially explained by a handful of features playing a crucial role ...
|
| |
In Workshop on Constraint Based Methods for Bioinformatics (2010)
posted to algorithm_portfolios
by bsilverthorn
on 2012-02-29 01:46:09
|
| |
Abstract
The importance of algorithm portfolio techniques for SAT has long been noted, and a number of very successful systems have been devised, including the most successful one—SATzilla. However, all these systems are quite complex (to understand, reimplement, or modify). In this paper we present an algorithm portfolio for SAT that is extremely simple, but in the same time so efficient that it outperforms SATzilla. For a new SAT instance to be solved, our portfolio finds its k -nearest neighbors from the ...
|
| |
In Applications of Topic Models Workshop at Neural Information Processing Systems (NIPS) (2009)
Abstract
A database of objects discovered in houses in the Roman city of Pompeii provides a unique view of ordinary life in an ancient city. Experts have used this collection to study the structure of Roman households, exploring the distribution and variability of tasks in architectural spaces, but such approaches are necessarily affected by modern cultural assumptions. In this study we present a data-driven approach to household archeology, treating it as an unsupervised labeling problem, that attempts to provide a more objective complement to human ...
|
| |
Abstract
We present a probabilistic generative model of entity relationships and textual attributes; the model simultaneously discovers groups among the entities and topics among the corresponding text. Block models of relationship data have been studied in social network analysis for some time, however here we cluster in multiple modalities at once. Significantly, joint inference allows the discovery of groups to be guided by the emerging topics, and vice-versa. We present experimental results on two large data sets: sixteen years of bills put ...
|
| |
Abstract
Non-deterministic polynomial time (commonly termed 'NP-complete') problems are relevant to many computational tasks of practical interest—such as the 'travelling salesman problem'—but are difficult to solve: the computing time grows exponentially with problem size in the worst case. It has recently been shown that these problems exhibit 'phase boundaries', across which dramatic changes occur in the computational difficulty and solution character—the problems become easier to solve away from the boundary. Here we report an analytic solution and experimental investigation of the phase ...
|
| |
In Fourteenth International Symposium on Practical Aspects of Declarative Languages (PADL) (2012)
posted to answer_set_programming
by bsilverthorn
on 2012-02-27 21:57:35
|
| |
posted to local_search satisfiability
by bsilverthorn
on 2012-02-24 17:09:58
Abstract
Stochastic local search (SLS) methods are well known for their ability to find models of randomly generated instances of the propositional satisfiability problem (SAT) very effectively. Two well-known SLS-based SAT solvers are Sparrow , one of the best-performing solvers for random 3-SAT instances, and VE-Sampler , which achieved significant performance improvements over previous SLS solvers on SAT-encoded software verification problems. Here, we introduce a new highly parametric algorithm, Captain Jack , which extends the parameter space of Sparrow to incorporate elements ...
|
| |
(2011)
posted to satisfiability slides
by bsilverthorn
on 2012-02-24 17:00:01
|
| |
(2011)
posted to satisfiability slides
by bsilverthorn
on 2012-02-24 16:51:18
|
| |
In Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI) (2010)
|
| |
In Proceedings of the 27th Conference on Uncertainty in Artificial Intelligence (UAI) (2011)
posted to markov_logic
by bsilverthorn
on 2012-02-24 05:34:01
|
| |
In Eighteenth National Conference on Artificial Intelligence (2002)
posted to max_sat
by bsilverthorn
on 2012-02-24 05:28:44
Abstract
Logical and probabilistic reasoning are Closely related. Many examples in each group have natural analogs in the other. One example is the strong relationship between weighted MAXSAT and MPE. This paper presents a simple reduction of MPE to weighted MAX-SAT. It also investigates approximating MPE by converting it to a weighted MAX-SAT problem, then using the incomplete methods for solving weighted MAX-SAT to generate a solution. We show that converting MPE problems to MAX-SAT problems and using a method designed for ...
|
| |
(2003)
Abstract
Knowledge management and knowledge-based intelligence are areas of importance in today's economy and society, and their exploitation requires representation via the development of a declarative interface whose input language is based on logic. Chitta Baral demonstrates how to write programs that behave intelligently by giving them the ability to express knowledge and reason about it. He presents a language, AnsProlog, for both knowledge representation and reasoning, and declarative problem solving. Many of the results have never appeared before in book form but are organized here for those wishing ...
|
| |
posted to answer_set_programming
by bsilverthorn
on 2012-02-24 05:10:09
|
| |
|
| |
Abstract
We describe the reconstruction of a phylogeny for a set of taxa, with a character-based cladistics approach, in a declarative knowledge representation formalism, and show how to use computational methods of answer set programming to generate conjectures about the evolution of the given taxa. We have applied this computational method in two domains: historical analysis of languages and historical analysis of parasite-host systems. In particular, using this method, we have computed some plausible phylogenies for Chinese dialects, for Indo-European language groups, ...
|
| |
Abstract
One of the strength of Eclipse, the well-known open platform for software development, is its extensibility made possible by the built-in pluggability mechanisms. However those pluggability mechanisms only reveal their full potential when extensions created by others are made easy to distribute and obtain. The purpose of Eclipse p2 project is to build a platform addressing the challenges of distribution and obtention of Eclipse and its extensions, which poses the same dependency management issues than for component based systems. This paper ...
|
| |
Abstract
Symbolic reasoning is in the core of many software development tools such as: bug-finders, test-case generators, and verifiers. Of renewed interest is the use of symbolic reasoning for synthesing code, loop invariants and ranking functions. Satisfiability Modulo Theories (SMT) solvers have been the focus of increased recent attention thanks to technological advances and an increasing number of applications. In this paper we review some of these applications that use software verifiers as bug-finders “on steroids” and suggest that new model finding ...
|
| |
In Workshop on Invariant Generation (WING) (2011)
|
| |
Abstract
The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in ...
|
| |
by Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, et al.Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik
Abstract
Formal verification of arithmetic datapaths has been part of the established methodology for most Intel processor designs over the last years, usually in the role of supplementing more traditional coverage oriented testing activities. For the recent Intel CoreTM i7 design we took a step further and used formal verification as the primary validation vehicle for the core execution cluster, the component responsible for the functional behaviour of all microinstructions. We applied symbolic simulation based formal verification techniques for full datapath, control ...
|
| |
Journal on Satisfiability, Boolean Modeling and Computation (2006)
Abstract
In this paper, we describe and evaluate three different techniques for translating pseudoboolean constraints (linear constraints over boolean variables) into clauses that can be handled by a standard SAT-solver. We show that by applying a proper mix of translation techniques, a SAT-solver can perform on a par with the best existing native pseudo-boolean solvers. This is particularly valuable in those cases where the constraint problem of interest is naturally expressed as a SAT problem, except for a handful of constraints. Translating ...
|
| |
Abstract
Answer set programming is a new programming paradigm proposed in [1] and [2], and based on the answer set semantics of Prolog [3]. It is well known that an answer set for a logic program is also a model of the program’s completion [4]. The converse is true when the logic program is “tight” [5,6]. Lin and Zhao [7] showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to ...
|
| |
In Proceedings of the 19th International Conference on Computer Aided Verification (2007)
Abstract
Rarely verification problems originate from bit-level descriptions. Yet, most of the verification technologies are based on bit blasting, i.e., reduction to boolean reasoning. In this paper we advocate reasoning at higher level of abstraction, within the theory of bit vectors (BV), where structural information (e.g. equalities, arithmetic functions) is not blasted into bits. Our approach relies on the lazy Satisfiability Modulo Theories (SMT) paradigm. We developed a satisfiability procedure for reasoning about bit vectors that carefully leverages on the power of ...
|
| |
In Proceedings of the 23rd National Conference on Artificial Intelligence (2008)
Abstract
Answer set programming (ASP) is a form of declarative programming oriented towards difficult search problems. As an outgrowth of research on the use of nonmonotonic reasoning in knowledge representation, it is particularly useful in knowledge-intensive applications. ASP programs consist of rules that look like Prolog rules, but the computational mechanisms used in ASP are different: they are based on the ideas that have led to the creation of fast satisfiability solvers for propositional logic. ...
|
| |
Abstract
Answer set programming (ASP) emerged in the late 1990s as a new logic programming paradigm that has been successfully applied in various application domains. Also motivated by the availability of efficient solvers for propositional satisfiability (SAT), various reductions from logic programs to SAT were introduced. All these reductions, however, are limited to a subclass of logic programs or introduce new variables or may produce exponentially bigger propositional formulas. In this paper, we present a SAT-based procedure, called ASPSAT, that (1) deals ...
|
| |
posted to satisfiability surveys
by bsilverthorn
on 2012-02-22 23:21:37
|
Search
