Sciweavers

193 search results - page 36 / 39
» sat 2007
Sort
View
CSR
2007
Springer
15 years 10 months ago
Ruling Out Polynomial-Time Approximation Schemes for Hard Constraint Satisfaction Problems
The maximum constraint satisfaction problem (Max CSP) is the following computational problem: an instance is a finite collection of constraints on a set of variables, and the goal...
Peter Jonsson, Andrei A. Krokhin, Fredrik Kuivinen
CSR
2007
Springer
15 years 10 months ago
New Bounds for MAX-SAT by Clause Learning
To solve a problem on a given CNF formula F a splitting algorithm recursively calls for F[v] and F[¬v] for a variable v. Obviously, after the first call an algorithm obtains some...
Alexander S. Kulikov, Konstantin Kutzkov
TABLEAUX
2007
Springer
15 years 10 months ago
Bounded Model Checking with Description Logic Reasoning
Abstract. Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the sys...
Shoham Ben-David, Richard J. Trefler, Grant E. Wed...
TACAS
2007
Springer
124views Algorithms» more  TACAS 2007»
15 years 10 months ago
Deciding Bit-Vector Arithmetic with Abstraction
ion Randal E. Bryant1 , Daniel Kroening2 , Jo¨el Ouaknine3 , Sanjit A. Seshia4 , Ofer Strichman5 , and Bryan Brady4 1 Carnegie Mellon University, Pittsburgh 2 ETH Z¨urich 3 Oxfor...
Randal E. Bryant, Daniel Kroening, Joël Ouakn...
ASPDAC
2007
ACM
139views Hardware» more  ASPDAC 2007»
15 years 7 months ago
Deeper Bound in BMC by Combining Constant Propagation and Abstraction
ound in BMC by Combining Constant Propagation and Abstraction Roy Armoni, Limor Fix1 , Ranan Fraer1 , Tamir Heyman1,3 , Moshe Vardi2 , Yakir Vizel1 , Yael Zbar1 1 Logic and Validat...
Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, ...