IEEEHPCS
2010
13 years 11 months ago
2010
Abstract. In this paper, we explore the two well-known principles of diversification and intensification in portfolio-based parallel SAT solving. These dual concepts play an impo...
BIRTHDAY
2010
Springer
14 years 1 months ago
2010
Springer
Abstract. We describe our progress building the program ReductionFinder, which uses off-the-shelf SAT solvers together with the Cmodels system to automatically search for reduction...
AAAI
2010
14 years 2 months ago
2010
Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretical...
CP
2005
Springer
14 years 2 months ago
2005
Springer
Boolean Constraint Propagation (BCP) is recognized as one of the most useful technique for efficient satisfiability checking. In this paper a new extension of the scope of boole...
ASPDAC
2005
ACM
14 years 2 months ago
2005
ACM
－ It is a hotly research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL algorithm is the most effective Counterexample minim...
AISC
2008
Springer
14 years 2 months ago
2008
Springer
Grid computing offers a promising approach to solving challenging computational problems in an environment consisting of a large number of easily accessible resources. In this pape...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
This work presents a memory-efficient All-SAT engine which, given a propositional formula over sets of important and non-important variables, returns the set of all the assignments...
ICCD
2000
IEEE
14 years 5 months ago
2000
IEEE
This paper presents a verification technique for functional comparison of large combinational circuits using a novel combination of known approaches. The idea is based on a tight...
KR
2010
Springer
14 years 5 months ago
2010
Springer
We present a distributed algorithm for computing equilibria of heterogeneous nonmonotonic multi-context systems (MCS). The algorithm can be parametrized to compute only partial eq...
MEMOCODE
2003
IEEE
14 years 6 months ago
2003
IEEE
— Modern SAT solvers have proved highly successful in finding counterexamples to temporal properties of systems, using a method known as ”bounded model checking”. It is natu...