Uniform Reduction to SAT

Details Uniform Reduction to SAT Uniform Reduction to SAT

2010-12-06

arxiv.org/abs/1012.1255v1

Computer Science

Artificial Intelligence

50 pages, uses tikz.sty

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Uniform Reduction to SAT does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Uniform Reduction to SAT, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Uniform Reduction to SAT will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-168399