Core-guided method for constraint-based multi-objective combinatorial optimization

  • PDF / 1,485,050 Bytes
  • 15 Pages / 595.224 x 790.955 pts Page_size
  • 84 Downloads / 198 Views

DOWNLOAD

REPORT


Core-guided method for constraint-based multi-objective combinatorial optimization Naiyu Tian1,3 · Dantong Ouyang1,3 · Yiyuan Wang2,3 · Yimou Hou1,3 · Liming Zhang1,3 Accepted: 1 October 2020 © Springer Science+Business Media, LLC, part of Springer Nature 2020

Abstract Multi-Objective Combinatorial Optimization(MOCO), which consists of several conflicting objectives to be optimized, finds an ever-increasing number of uses in many real-world applications. In past years, the research of MOCO mainly focuses on evolutionary algorithms. Recently, constraint-based methods come into the view and have been proved to be effective on MOCO problems. This paper builds on the previous works of constraint-based algorithm MCSEnumPD(AAAI18) using path diversification method. Due to the inadequacy that the original method fails to prune the redundant search space effectively, this paper proposes the definition of infeasible path and develops a novel algorithm that exploits the properties of unsatisfiable cores, referred as CgPDMCS. The approach extends MCSEnumPD algorithm with a core-guided path diversification method, which avoids solving infeasible paths representing the supersets of the unsatisfiable cores. Experimental results show that the novel approach provides further performance gains over the previous constraint-based algorithms, especially for the instances tightly constrained. Keywords Constraint · SAT · Minimal correction set · Multi-objective combinatorial optimization · Pareto front

1 Introduction In recent years, Propositional Satisfiability (SAT) has attracted considerable attention in the fields of academia and industry and has made a significant advancement [1– 6]. As the first proved Non-deterministic Polynomial (NP) complete problem, SAT is the seed problem in the theory of NP-complete, which has great theoretical and practical significance. Since, SAT is always expressed in Boolean logic, various real-world problems may be compiled to Satisfiability instances, such as synthesis [7], gate level circuits debugging [8], model-based diagnosis problem [9], and multi-robot motion planning problems [10]. In virtue of the SAT competition held every year, these problems are able to be solved effectively by growing SAT solvers This work is supported by the National Natural Science Foundation of China (Grant Nos. 61672261, 61872159,61806050, 61972063) and Fundamental Research Funds for the Central Universities 2412020FZ030, Jilin Education Department JJKH20190289KJ.  Liming Zhang

[email protected]

Extended author information available on the last page of the article.

[11, 12]. Integrating SAT solvers into algorithms for solving optimization problems has also produced a new generation of efficient tools. Central to the research for analyzing infeasible instances or the analysis of overconstrained systems is the task of extracting a single feature or result from an instance, such as a Maximal Satisfiable Subset (MSS), a Minimal Unsatisfiable Subset (MUS) or a Minimal Correction Set (MCS). The subsets provide imp