Skip to Main content Skip to Navigation
Conference papers

Relaxation search: a simple way of managing optional clauses

Abstract : A number of problems involve managing a set of optional clauses. For example, the soft clauses in a MAXSAT formula are optional—they can be falsified for a cost. Similarly, when computing a Minimum Correction Set for an unsatisfiable formula, all clauses are optional—some can be falsified in order to satisfy the remaining. In both of these cases the task is to find a subset of the optional clauses that achieves some criteria, and whose removal leaves a satisfiable formula. Relaxation search is a simple method of using a standard SAT solver to solve this task. Relaxation search is easy to implement, sometimes requiring only a simple modification of the variable selection heuristic in the SAT solver; it offers considerable flexibility and control over the order in which subsets of optional clauses are examined; and it automatically exploits clause learning to exchange information between the two phases of finding a suitable subset of optional clauses and checking if their removal yields satisfiability. We demonstrate how relaxation search can be used to solve MAXSAT and to compute Minimum Correction Sets. In both cases relaxation search is able to achieve state-of-the-art performance and solve some instances other solvers are not able to solve.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inrae.fr/hal-02738910
Contributor : Migration Prodinra Connect in order to contact the contributor
Submitted on : Tuesday, June 2, 2020 - 9:22:47 PM
Last modification on : Wednesday, May 12, 2021 - 8:11:18 AM
Long-term archiving on: : Friday, December 4, 2020 - 5:23:19 PM

File

Relaxation search_a simple way...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02738910, version 1
  • PRODINRA : 263230

Collections

Citation

Fahiem Bacchus, Jessica Davies, Maria Tsimpoukelli, George Katsirelos. Relaxation search: a simple way of managing optional clauses. AAAI 2014 - 28th AAAI Conference, Association for the Advancement of Artificial Intelligence (AAAI). USA., Jul 2014, Québec, Canada. 7 p. ⟨hal-02738910⟩

Share

Metrics

Les métriques sont temporairement indisponibles