| Satisfiability research (SAT) is a core discipline connecting topics in Discrete Mathematics, Complexity theory, hard-and software verification, circuit design- and testing and Statistical Physics .Last years have shown an increasing interest and frequency of conferences (http://www.satisfiability.org/) and publications in this area. This latter fact resulted recently in the setup of a new Journal (http://www.isa.ewi.tudelft.nl/Jsat/). A yearly SAT-solver contest started in 2002 (http://www.satcompetition.org/). The emerging success of SAT solvers is largely based on the fact that very efficient data structures and use of cache optimizations are possible when reasoning with CNF formulas. The failure of extended solving methods, as Integer Programming, Pseudo-Boolean Programming and Constraint Programming in their full versions, when dealing with large scale discrete problems is likewise explained by the lack of this possibility. We propose to develop a solver based on reasoning with cardinality constraints only. Such a solver can be situated halfway a SAT Solver and a Pseudo-Boolean Solver, aiming to keep as much of the optimized use of data structures and resolution based principles from SAT and to benefit from the much richer modeling capacities cardinality constraints allow, at the same time avoiding the very costly handling with integer coefficients. |
