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) ...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.展开更多
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.展开更多
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.展开更多
Model-based diagnosis(MBD)with multiple observations shows its significance in identifying fault location.The existing approaches for MBD with multiple observations use observations which is inconsistent with the pred...Model-based diagnosis(MBD)with multiple observations shows its significance in identifying fault location.The existing approaches for MBD with multiple observations use observations which is inconsistent with the prediction of the system.In this paper,we proposed a novel diagnosis approach,namely,the Diagnosis with Different Observations(DiagDO),to exploit the diagnosis when given a set of pseudo normal observations and a set of abnormal observations.Three ideas are proposed in this paper.First,for each pseudo normal observation,we propagate the value of system inputs and gain fanin-free edges to shrink the size of possible faulty components.Second,for each abnormal observation,we utilize filtered nodes to seek surely normal components.Finally,we encode all the surely normal components and parts of dominated components into hard clauses and compute diagnosis using the MaxSAT solver and MCS algorithm.Extensive tests on the ISCAS'85 and ITC'99 benchmarks show that our approach performs better than the state-of-the-art algorithms.展开更多
基金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.
基金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 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.
基金supported by the National Natural Science Foundation of China(Grant Nos.62076108,61972360,and 61872159).
文摘Model-based diagnosis(MBD)with multiple observations shows its significance in identifying fault location.The existing approaches for MBD with multiple observations use observations which is inconsistent with the prediction of the system.In this paper,we proposed a novel diagnosis approach,namely,the Diagnosis with Different Observations(DiagDO),to exploit the diagnosis when given a set of pseudo normal observations and a set of abnormal observations.Three ideas are proposed in this paper.First,for each pseudo normal observation,we propagate the value of system inputs and gain fanin-free edges to shrink the size of possible faulty components.Second,for each abnormal observation,we utilize filtered nodes to seek surely normal components.Finally,we encode all the surely normal components and parts of dominated components into hard clauses and compute diagnosis using the MaxSAT solver and MCS algorithm.Extensive tests on the ISCAS'85 and ITC'99 benchmarks show that our approach performs better than the state-of-the-art algorithms.