Sciweavers

CONSTRAINTS
2010
126views more  CONSTRAINTS 2010»
13 years 1 months ago
Solving satisfiability problems with preferences
Abstract. Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different ...
Emanuele Di Rosa, Enrico Giunchiglia, Marco Marate...
AIPS
2006
13 years 6 months ago
Lemma Reusing for SAT based Planning and Scheduling
In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches generate a sequence of SAT prob...
Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, K...
CP
2008
Springer
13 years 6 months ago
A New Empirical Study of Weak Backdoors
Abstract. Work by Kilby, Slaney, Thiebaux and Walsh [1] showed that the backdoors and backbones of unstructured Random 3SAT instances are largely disjoint. In this work we extend t...
Peter Gregory, Maria Fox, Derek Long
ECAI
2006
Springer
13 years 6 months ago
Solving Optimization Problems with DLL
Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different applicati...
Enrico Giunchiglia, Marco Maratea
AIPS
2008
13 years 6 months ago
The Complexity of Optimal Planning and a More Efficient Method for Finding Solutions
We present a faster method of solving optimal planning problems and show that our solution performs up to an order of magnitude faster than Satplan on a variety of problems from t...
Katrina Ray, Matthew L. Ginsberg
DATE
2004
IEEE
175views Hardware» more  DATE 2004»
13 years 8 months ago
Breaking Instance-Independent Symmetries in Exact Graph Coloring
Code optimization and high level synthesis can be posed as constraint satisfaction and optimization problems, such as graph coloring used in register allocation. Graph coloring is...
Arathi Ramani, Fadi A. Aloul, Igor L. Markov, Kare...
CP
2003
Springer
13 years 9 months ago
Unrestricted Nogood Recording in CSP Search
Recently spectacular improvements in the performance of SAT solvers have been achieved through nogood recording (clause learning). In the CSP literature, on the other hand, nogood ...
George Katsirelos, Fahiem Bacchus
MTV
2003
IEEE
126views Hardware» more  MTV 2003»
13 years 9 months ago
Heuristic Backtracking Algorithms for SAT
In recent years backtrack search SAT solvers have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully replace BDDs in many areas of f...
Ateet Bhalla, Inês Lynce, José T. de ...
SAT
2004
Springer
99views Hardware» more  SAT 2004»
13 years 10 months ago
Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables
We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empir...
Carlos Ansótegui, Felip Manyà
SAT
2005
Springer
142views Hardware» more  SAT 2005»
13 years 10 months ago
Optimizations for Compiling Declarative Models into Boolean Formulas
Advances in SAT solver technology have enabled many automated analysis and reasoning tools to reduce their input problem to a SAT problem, and then to use an efficient SAT solver ...
Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, L...