You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Solving Weighted Max-SAT Problems in a Reduced Search Space: A Performance Analysis1

Issue title: 2007 Competitions

Guest editors: Ewald Speckenmeyer, Chu Min Li, Vasco Manquinho and Armando Tacchella

Article type: Research Article

Authors: Pipatsrisawat, Knot | Palyan, Akop | Chavira, Mark | Choi, Arthur | Darwiche, Adnan

Affiliations: Department of Computer Science, University of California, Los Angeles. E-mails: darwiche@cs.ucla.edu, apalyan@ucla.edu, chavira@cs.ucla.edu, aychoi@cs.ucla.edu

Note: [1] This work extends our previous work in [38].

Keywords: Max-SAT, constraint relaxation, lower bound computation

DOI: 10.3233/SAT190044

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 191-217, 2008

Received 1 October 2007
|
Revision received 1 February 2008
|
Published: 1 June 2008
Get PDF open access

Abstract

We analyze, in this work, the performance of a recently introduced weighted Max-SAT solver, Clone, in the Max-SAT evaluation 2007. Clone utilizes a novel bound computation based on formula compilation that allows it to search in a reduced search space. We study how additional techniques from the SAT and Max-SAT literature affect the performance of Clone on problems from the evaluation. We then perform further investigations on factors that may affect the performance of leading Max-SAT solvers. We empirically identify two properties of weighted Max-SAT problems that can be used to adjust the difficulty level of the problems with respect to the considered solvers.

Show more