The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most loca...The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.展开更多
Distributed Integrated Modular Avionics(DIMA)develops from Integrated Modular Avionics(IMA)and realizes distributed integration of multiple sub-function areas.Timetriggered network provides effective support for time ...Distributed Integrated Modular Avionics(DIMA)develops from Integrated Modular Avionics(IMA)and realizes distributed integration of multiple sub-function areas.Timetriggered network provides effective support for time synchronization and information coordination in DIMA systems.However,inconsistency between processing resources and communication network destroys the time determinism benefiting from partitions and time-triggered mechanism.To ensure such time determinism and achieve guaranteed real-time performance,system design should collectively provide a global communication scheme for messages in network domain and a corresponding execution scheme for partitions in processing domain.This paper firstly establishes a general DIMA model which coordinates partitioned processing and time-triggered communication,and then proposes a hybrid scheduling algorithm using Mixed Integer Programming to produce feasible system schemes.Furthermore,incrementally integrating new functions causes upgrades or reconfigurations of DIMA systems and will generate integration cost.To control such cost,this paper further develops an optimization algorithm based on Maximum Satisfiability Problem and guarantees that the scheduling design for upgraded DIMA systems inherit their original schemes as much as possible.Finally,two typical cases,including a simple fully connected DIMA system case and an industrial DIMA system case,are constructed to illustrate our DIMA model and validate the effectiveness of our hybrid scheduling algorithms.展开更多
The maximum satisfiability (MAX-SAT)problem is an important NP-hard problem in theory,and has a broad range of applications in practice.Stochastic local search (SLS)is becoming an increasingly popular method for solvi...The maximum satisfiability (MAX-SAT)problem is an important NP-hard problem in theory,and has a broad range of applications in practice.Stochastic local search (SLS)is becoming an increasingly popular method for solving MAX-SAT.Recently,a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances.However,the performance of CCLS on solving industrial MAX-SAT instances lags far behind.In this paper,we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances.First,we conduct experiments to analyze why CCLS performs poor on industrial instances.Then we propose a new strategy called additive BMS (Best from Multiple Selections)to ease the serious issue.By integrating CCLS and additive BMS,we develop a new SLS algorithm for MAXSAT called CCABMS,and related experiments indicate the efficiency of CCABMS.Also,we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT,and combine an effective initialization method with CCABMS,resulting in an enhanced algorithm.Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.展开更多
Static compaction methods aim at finding unnecessary test patterns to reduce the size of the test set as a post-process of test generation.Techniques based on partial maximum satisfiability are often used to track man...Static compaction methods aim at finding unnecessary test patterns to reduce the size of the test set as a post-process of test generation.Techniques based on partial maximum satisfiability are often used to track many hard problems in various domains,including artificial intelligence,computational biology,data mining,and machine learning.We observe that part of the test patterns generated by the commercial Automatic Test Pattern Generation(ATPG)tool is redundant,and the relationship between test patterns and faults,as a significant information,can effectively induce the test patterns reduction process.Considering a test pattern can detect one or more faults,we map the problem of static test compaction to a partial maximum satisfiability problem.Experiments on ISCAS89,ISCAS85,and ITC99 benchmarks show that this approach can reduce the initial test set size generated by TetraMAX18 while maintaining fault coverage.展开更多
Based on our recent study on probability distributions for evolution in extremal optimization(EO),we propose a modified framework called EOSAT to approximate ground states of the hard maximum satisfiability(MAXSAT)pro...Based on our recent study on probability distributions for evolution in extremal optimization(EO),we propose a modified framework called EOSAT to approximate ground states of the hard maximum satisfiability(MAXSAT)problem,a generalized version of the satisfiability(SAT)problem.The basic idea behind EOSAT is to generalize the evolutionary probability distribution in the Bose-Einstein-EO(BE-EO)algorithm,competing with other popular algorithms such as simulated annealing and WALKSAT.Experimental results on the hard MAXSAT instances from SATLIB show that the modified algorithms are superior to the original BE-EO algorithm.展开更多
选择一组能够检测并隔离所有故障的故障检测隔离集(FDIS)是动态系统基于模型故障检测与隔离(FDI)的重要步骤,该步骤通常要求FDIS的基数最小,即求解最小故障检测隔离集(MFDIS),MFDIS的求解时间随着问题规模增大呈指数级增长。BILP(Binary...选择一组能够检测并隔离所有故障的故障检测隔离集(FDIS)是动态系统基于模型故障检测与隔离(FDI)的重要步骤,该步骤通常要求FDIS的基数最小,即求解最小故障检测隔离集(MFDIS),MFDIS的求解时间随着问题规模增大呈指数级增长。BILP(Binary integer linear programming)完备方法是现行动态系统中通用和最高效的MFDIS求解方法,但该方法的求解效率有待提高。本文首次提出了基于部分最大可满足性问题(PMS)的MFDIS求解方法。提出极小超定方程集(MSO)的概念,将部分MSO集合用MSO等价集表示,以缩减问题规模。将MFDIS求解问题转化为PMS问题,进而提高求解效率。实验结果表明,本文方法将问题规模平均约简至原来的8.22%;与BILP方法相比,本文方法的求解效率提高了4.18~9.5倍。展开更多
Combinatorial optimization(CO)on graphs is a classic topic that has been extensively studied across many scientific and industrial fields.Recently,solving CO problems on graphs through learning methods has attracted g...Combinatorial optimization(CO)on graphs is a classic topic that has been extensively studied across many scientific and industrial fields.Recently,solving CO problems on graphs through learning methods has attracted great attention.Advanced deep learning methods,e.g.,graph neural networks(GNNs),have been used to effectively assist the process of solving COs.However,current frameworks based on GNNs are mainly designed for certain CO problems,thereby failing to consider their transferable and generalizable abilities among different COs on graphs.Moreover,simply using original graphs to model COs only captures the direct correlations among objects,which does not consider the mathematical logicality and properties of COs.In this paper,we propose a unified pre-training and adaptation framework for COs on graphs with the help of the maximum satisfiability(Max-SAT)problem.We first use Max-SAT to bridge different COs on graphs since they can be converted to Max-SAT problems represented by standard formulas and clauses with logical information.Then we further design a pre-training and domain adaptation framework to extract the transferable and generalizable features so that different COs can benefit from them.In the pre-training stage,Max-SAT instances are generated to initialize the parameters of the model.In the fine-tuning stage,instances from CO and Max-SAT problems are used for adaptation so that the transferable ability can be further improved.Numerical experiments on several datasets show that features extracted by our framework exhibit superior transferability and Max-SAT can boost the ability to solve COs on graphs.展开更多
文摘The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.
基金co-supported by the National Natural Science Foundation of China(No.71701020)the Defense Research Field Foundation of China(No.61403120404)the Civil Aircraft Airworthiness and Maintenance Key Laboratory Fund of Civil Aviation University of China(No.2017SW02).
文摘Distributed Integrated Modular Avionics(DIMA)develops from Integrated Modular Avionics(IMA)and realizes distributed integration of multiple sub-function areas.Timetriggered network provides effective support for time synchronization and information coordination in DIMA systems.However,inconsistency between processing resources and communication network destroys the time determinism benefiting from partitions and time-triggered mechanism.To ensure such time determinism and achieve guaranteed real-time performance,system design should collectively provide a global communication scheme for messages in network domain and a corresponding execution scheme for partitions in processing domain.This paper firstly establishes a general DIMA model which coordinates partitioned processing and time-triggered communication,and then proposes a hybrid scheduling algorithm using Mixed Integer Programming to produce feasible system schemes.Furthermore,incrementally integrating new functions causes upgrades or reconfigurations of DIMA systems and will generate integration cost.To control such cost,this paper further develops an optimization algorithm based on Maximum Satisfiability Problem and guarantees that the scheduling design for upgraded DIMA systems inherit their original schemes as much as possible.Finally,two typical cases,including a simple fully connected DIMA system case and an industrial DIMA system case,are constructed to illustrate our DIMA model and validate the effectiveness of our hybrid scheduling algorithms.
基金the National Key Research and Development Program of China (2016YFE0100300, 2017YFB02025)partially supported by the 100 Talents Program of the Chinese Academy of Sciences (2920154070)+2 种基金partially supported by the Knowledge Innovation Project of the Chinese Academy of Sciences (5120146040)partially supported by the Open Project Program of the State Key Laboratory of Mathematical Engineering and Advanced Computing (2016A06)partially supported by the National Natural Science Foundation of China (Grant No.61502464).
文摘The maximum satisfiability (MAX-SAT)problem is an important NP-hard problem in theory,and has a broad range of applications in practice.Stochastic local search (SLS)is becoming an increasingly popular method for solving MAX-SAT.Recently,a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances.However,the performance of CCLS on solving industrial MAX-SAT instances lags far behind.In this paper,we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances.First,we conduct experiments to analyze why CCLS performs poor on industrial instances.Then we propose a new strategy called additive BMS (Best from Multiple Selections)to ease the serious issue.By integrating CCLS and additive BMS,we develop a new SLS algorithm for MAXSAT called CCABMS,and related experiments indicate the efficiency of CCABMS.Also,we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT,and combine an effective initialization method with CCABMS,resulting in an enhanced algorithm.Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.
基金supported by the National Natural Science Foundation of China(Nos.61672261 and 61872159)。
文摘Static compaction methods aim at finding unnecessary test patterns to reduce the size of the test set as a post-process of test generation.Techniques based on partial maximum satisfiability are often used to track many hard problems in various domains,including artificial intelligence,computational biology,data mining,and machine learning.We observe that part of the test patterns generated by the commercial Automatic Test Pattern Generation(ATPG)tool is redundant,and the relationship between test patterns and faults,as a significant information,can effectively induce the test patterns reduction process.Considering a test pattern can detect one or more faults,we map the problem of static test compaction to a partial maximum satisfiability problem.Experiments on ISCAS89,ISCAS85,and ITC99 benchmarks show that this approach can reduce the initial test set size generated by TetraMAX18 while maintaining fault coverage.
基金supported by the National Natural Science Foundation of China(No.61074045)the National Basic Research Program(973)of China(No.2007CB714000)the National Creative Research Groups Science Foundation of China(No.60721062)
文摘Based on our recent study on probability distributions for evolution in extremal optimization(EO),we propose a modified framework called EOSAT to approximate ground states of the hard maximum satisfiability(MAXSAT)problem,a generalized version of the satisfiability(SAT)problem.The basic idea behind EOSAT is to generalize the evolutionary probability distribution in the Bose-Einstein-EO(BE-EO)algorithm,competing with other popular algorithms such as simulated annealing and WALKSAT.Experimental results on the hard MAXSAT instances from SATLIB show that the modified algorithms are superior to the original BE-EO algorithm.
文摘选择一组能够检测并隔离所有故障的故障检测隔离集(FDIS)是动态系统基于模型故障检测与隔离(FDI)的重要步骤,该步骤通常要求FDIS的基数最小,即求解最小故障检测隔离集(MFDIS),MFDIS的求解时间随着问题规模增大呈指数级增长。BILP(Binary integer linear programming)完备方法是现行动态系统中通用和最高效的MFDIS求解方法,但该方法的求解效率有待提高。本文首次提出了基于部分最大可满足性问题(PMS)的MFDIS求解方法。提出极小超定方程集(MSO)的概念,将部分MSO集合用MSO等价集表示,以缩减问题规模。将MFDIS求解问题转化为PMS问题,进而提高求解效率。实验结果表明,本文方法将问题规模平均约简至原来的8.22%;与BILP方法相比,本文方法的求解效率提高了4.18~9.5倍。
基金supported by National Natural Science Foundation of China(Grant Nos.11991021,11991020 and 12271503)。
文摘Combinatorial optimization(CO)on graphs is a classic topic that has been extensively studied across many scientific and industrial fields.Recently,solving CO problems on graphs through learning methods has attracted great attention.Advanced deep learning methods,e.g.,graph neural networks(GNNs),have been used to effectively assist the process of solving COs.However,current frameworks based on GNNs are mainly designed for certain CO problems,thereby failing to consider their transferable and generalizable abilities among different COs on graphs.Moreover,simply using original graphs to model COs only captures the direct correlations among objects,which does not consider the mathematical logicality and properties of COs.In this paper,we propose a unified pre-training and adaptation framework for COs on graphs with the help of the maximum satisfiability(Max-SAT)problem.We first use Max-SAT to bridge different COs on graphs since they can be converted to Max-SAT problems represented by standard formulas and clauses with logical information.Then we further design a pre-training and domain adaptation framework to extract the transferable and generalizable features so that different COs can benefit from them.In the pre-training stage,Max-SAT instances are generated to initialize the parameters of the model.In the fine-tuning stage,instances from CO and Max-SAT problems are used for adaptation so that the transferable ability can be further improved.Numerical experiments on several datasets show that features extracted by our framework exhibit superior transferability and Max-SAT can boost the ability to solve COs on graphs.
