Sciweavers

29
Voted
JAR
2000
90views more  JAR 2000»
13 years 9 months ago
Resolution versus Search: Two Strategies for SAT
The paper compares two popular strategies for solving propositional satis ability, backtracking search and resolution, and analyzes the complexity of a directional resolution algo...
Irina Rish, Rina Dechter
JAR
2000
149views more  JAR 2000»
13 years 9 months ago
Guided Local Search for Solving SAT and Weighted MAX-SAT Problems
In this paper, we show how Guided Local Search (GLS) can be applied to the SAT problem and show how the resulting algorithm can be naturally extended to solve the weighted MAX-SAT ...
Patrick Mills, Edward P. K. Tsang
JAR
2000
145views more  JAR 2000»
13 years 9 months ago
Logical Cryptanalysis as a SAT Problem
Cryptographic algorithms play a key role in computer security and the formal analysis of their robustness is of utmost importance. Yet, logic and automated reasoning tools are seld...
Fabio Massacci, Laura Marraro
JAR
2000
50views more  JAR 2000»
13 years 9 months ago
Single Step Tableaux for Modal Logics
Fabio Massacci
JAR
2000
77views more  JAR 2000»
13 years 9 months ago
Proving Consistency Assertions for Automotive Product Data Management
We present a formal specification and verification approach for industrial product data bases containing Boolean logic formulae to express constraints. Within this framework, globa...
Wolfgang Küchlin, Carsten Sinz
JAR
2000
87views more  JAR 2000»
13 years 9 months ago
Managing Structural Information by Higher-Order Colored Unification
Dieter Hutter, Michael Kohlhase
JAR
2000
123views more  JAR 2000»
13 years 9 months ago
Local Search Algorithms for SAT: An Empirical Evaluation
Local search algorithms are among the standard methods for solving hard combinatorial problems from various areas of Artificial Intelligence and Operations Research. For SAT, some ...
Holger H. Hoos, Thomas Stützle
JAR
2000
129views more  JAR 2000»
13 years 9 months ago
Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems
We study the runtime distributions of backtrack procedures for propositional satisfiability and constraint satisfaction. Such procedures often exhibit a large variability in perfor...
Carla P. Gomes, Bart Selman, Nuno Crato, Henry A. ...
JAR
2000
97views more  JAR 2000»
13 years 9 months ago
A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering
We report our effort to build a geometry deductive database, which can be used to find the fixpoint for a geometric configuration. The system can find all the properties of the con...
Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang
JAR
2000
137views more  JAR 2000»
13 years 9 months ago
A Benchmark Method for the Propositional Modal Logics K, KT, S4
A lot of methods have been proposed -- and sometimes implemented -- for proof search in the propositional modal logics K, KT, and S4. It is difficult to compare the usefulness of ...
Peter Balsiger, Alain Heuerding, Stefan Schwendima...