Title :
Using interval constraint propagation for pseudo-Boolean constraint solving
Author :
Scheibler, Karsten ; Becker, B.
Author_Institution :
Univ. of Freiburg, Freiburg, Germany
Abstract :
This work is motivated by (1) a practical application which automatically generates test patterns for integrated circuits and (2) the observation that off-the-shelf state-of-the-art pseudo-Boolean solvers have difficulties in solving instances with huge pseudo-Boolean constraints as created by our application. Derived from the SMT solver iSAT3 we present the solver iSAT3p that on the one hand allows the efficient handling of huge pseudo-Boolean constraints with several thousand summands and large integer coefficients. On the other hand, experimental results demonstrate that at the same time iSAT3p is competitive or even superior to other solvers on standard pseudo-Boolean benchmark families.
Keywords :
Boolean functions; computability; automatic test pattern generation; iSAT3 SMT solver; iSAT3p solver; integer coefficients; integrated circuits; interval constraint propagation; pseudoBoolean constraint solving; pseudoBoolean solvers; standard pseudoBoolean benchmark; Benchmark testing; Boolean functions; Circuit faults; Data structures; Encoding; Integrated circuits; Iterative closest point algorithm;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2014
Conference_Location :
Lausanne
DOI :
10.1109/FMCAD.2014.6987614