Abstract

Propositional logic, with the aid of SAT solvers, has become capable of solving a range of important and complicated problems. Expanding this range, to contain additional varieties of problems, is subject to the complexity resulting from encoding counting constraints in conjunctive normal form. Due to the limitation of the expressive power of propositional logic, generally, such an encoding increases the numbers of variables and clauses excessively. This work eliminates the indicated drawback by interpolating constraint symbols and the set of natural numbers \ into the alphabet of propositional logic and adjusting the underlying language accordingly. In the extended logic counting constraints are naturally formulated, while many important aspects, such as Boolean nature and the soundness and completeness theorems, are kept preserved.