abstract bibtex

There is a huge number of problems, from various areas, being solved by reducing them to SAT. However, for most applications, translations into SAT are performed by specialized, problem-specific tools. In this paper we describe a novel approach for uniform solving of a wide class of problems by reducing them to SAT. The approach uses a new specification language that combines imperative and declarative programming paradigms. A problem is specified by a test (expressed in an imperative form) that a given set of values indeed makes a solution to the problem. In the solving phase, parameters of the problem are represented by (finite) vectors of propositional formulae and the specification is symbolically executed. An assertion that given values make a solution is transformed to an instance of the SAT problem and passed to a SAT solver. If the formula is satisfiable, its model is transformed back to variables describing the problem, i.e., to a solution of the problem. We also describe a system URSA that implements the described approach. The experiments show that the system is competitive to state-of-the related modelling systems.

@Article{Janicic2010, author = {Janicic, Predrag}, title = {Uniform Reduction to SAT}, journal = {arXiv}, volume = {cs.AI}, number = {}, pages = {}, year = {2010}, abstract = {There is a huge number of problems, from various areas, being solved by reducing them to SAT. However, for most applications, translations into SAT are performed by specialized, problem-specific tools. In this paper we describe a novel approach for uniform solving of a wide class of problems by reducing them to SAT. The approach uses a new specification language that combines imperative and declarative programming paradigms. A problem is specified by a test (expressed in an imperative form) that a given set of values indeed makes a solution to the problem. In the solving phase, parameters of the problem are represented by (finite) vectors of propositional formulae and the specification is symbolically executed. An assertion that given values make a solution is transformed to an instance of the SAT problem and passed to a SAT solver. If the formula is satisfiable, its model is transformed back to variables describing the problem, i.e., to a solution of the problem. We also describe a system URSA that implements the described approach. The experiments show that the system is competitive to state-of-the related modelling systems.}, location = {}, keywords = {cs.AI}}

Downloads: 0