Modeling and Solving Semiring Constraint Satisfaction Problems by Transformation to Weighted Semiring Max-SAT
We present a variant of the Weighted Maximum Satisfiability Problem (Weighted Max-SAT), which is a modeling of the Semiring Constraint Satisfaction framework. We show how to encode a Semiring Constraint Satisfaction Problem (SCSP) into an instance of a pr
- PDF / 435,444 Bytes
- 11 Pages / 430 x 660 pts Page_size
- 50 Downloads / 196 Views
DSL, SCSSE, University of Wollongong, Australia and DPSS, CSIR, South Africa 2 NICTA and ANU, Canberra, Australia 3 Meraka Institute, CSIR, Pretoria, South Africa 4 DSL, SCSSE, University of Wollongong, Australia
Abstract. We present a variant of the Weighted Maximum Satisfiability Problem (Weighted Max-SAT), which is a modeling of the Semiring Constraint Satisfaction framework. We show how to encode a Semiring Constraint Satisfaction Problem (SCSP) into an instance of a propositional Weighted Max-SAT, and call the encoding Weighted Semiring Max-SAT (WS-Max-SAT). The clauses in our encoding are highly structured and we exploit this feature to develop two algorithms for solving WS-MaxSAT: an incomplete algorithm based on the well-known GSAT algorithm for Max-SAT, and a branch-and-bound algorithm which is complete. Our preliminary experiments show that the translation of SCSP into WSMax-SAT is feasible, and that our branch-and-bound algorithm performs surprisingly well. We aim in future to combine the natural flexible representation of the SCSP framework with the inherent efficiencies of SAT solvers by adjusting existing SAT solvers to solve WS-Max-SAT.
1
Introduction
The Semiring Constraint Satisfaction Problem (SCSP) framework is an approach to constraint satisfaction and optimization that generalises classical Constraint Satisfaction Problems (CSPs), Partial Constraint Satisfaction Problems, Fuzzy CSPs, Weighted CSPs, Probabilistic CSPs, and others (over finite domains) [1,2,3,4], while also permitting the specification of interesting new instances. Considerable interest has been shown in solving SCSPs. Complete methods exist [5,6,7] but are likely to require exponential time. Bistarelli et al. [8] present a prototype SCSP solver based on an incomplete local search method. Wilson [9] shows how to use decision diagrams to solve SCSPs but provides no implementation. A significant amount of work has been devoted to solving propositional satisfiability (SAT) problems, and specifically the well-known maximum satisfiability problem (Max-SAT) [10,11]. There is continuing interest in translations between
NICTA is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.
M.A. Orgun and J. Thornton (Eds.): AI 2007, LNAI 4830, pp. 202–212, 2007. c Springer-Verlag Berlin Heidelberg 2007
Modeling and Solving Semiring Constraint Satisfaction Problems
203
CSPs and SAT problems [12,13,14]. This prompted us to explore the application of methods for solving Max-SAT to SCSPs. We modify the support encoding of CSP to SAT by Gent [12] in order to translate SCSPs as a variant of the Weighted Max-SAT Problem, and call this encoding WS-Max-SAT. Our encoding results in propositional clauses whose structure can be exploited in our algorithms to solve WS-Max-SAT: a local search algorithm that is a modification of the GSAT algorithm for solving Max-SAT [15], and a branch-and-bound (BnB) algorithm. We show how to formulate a SCSP as a WS-Max-SAT, present a local sea
Data Loading...
