SAT 2004 START ConferenceManager    


Problem encoding into SAT : the counting constraints case

Olivier Bailleux and Yacine Boufkhad

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

Many problems are naturally expressed using CNF clauses and Boolean cardinality constraints. It is generally believed that solving such problems through pure CNF encoding is inefficient, so many authors has proposed specialized algorithms : the pseudo-boolean solvers. In this paper we show that an appropriate pure CNF encoding can be competitive with these specialized methods. In conjunction with our encoding, we propose a slight modification of the DLL procedure that allows any DLL-based SAT solver to solve Boolean cardinality optimization problems. We show experimentally that our encoding allows zchaff to be competitive with pseudo-boolean solvers on some decision and optimization problems.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com