4.1 Article

Machine Learning Methods in Solving the Boolean Satisfiability Problem

相关参考文献

注意:仅列出部分参考文献,下载原文获取全部文献信息。
Article Computer Science, Hardware & Architecture

A Comprehensive Survey on Electronic Design Automation and Graph Neural Networks: Theory and Applications

Daniela Sanchez et al.

Summary: Driven by Moore's law, chip design complexity is increasing steadily. Electronic Design Automation (EDA) can handle the challenges of very large-scale integration and ensure scalability, reliability, and timely market introduction. However, EDA approaches are time and resource demanding, often without guaranteeing optimal solutions. To address this, Machine Learning (ML) has been integrated into various stages of the design flow, including placement and routing. Graph Neural Networks (GNNs) provide an opportunity to directly solve EDA problems using graph structures. This article comprehensively reviews the existing works linking EDA flow and GNNs, mapping them to a design pipeline, analyzing their practical implications, and summarizing the challenges faced when applying GNNs in the EDA design flow.

ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS (2023)

Article Computer Science, Artificial Intelligence

A survey for solving mixed integer programming via machine learning

Jiayi Zhang et al.

Summary: This paper surveys the trend of using machine learning to solve mixed-integer programming problems. Machine learning methods can provide solutions based on patterns from training data. The integration of machine learning and mixed-integer programming is discussed, including both exact and heuristic algorithms. The outlook for learning-based solvers, the expansion to other combinatorial optimization problems, and the embrace of traditional solvers and machine learning components are proposed. A list of papers utilizing machine learning technologies for combinatorial optimization problems is maintained.

NEUROCOMPUTING (2023)

Article Computer Science, Theory & Methods

On the Structure of the Boolean Satisfiability Problem: A Survey

Tasniem Nasser Alyahya et al.

Summary: The Boolean satisfiability problem (SAT) is a fundamental NP-complete decision problem, and SAT solvers' performance may vary due to the underlying structure of SAT instances. Previous studies have attempted to define the structure of SAT using measures such as phase transition, backbones, backdoors, small-world, scale-free, treewidth, centrality, community, self-similarity, and entropy, but the empirical evidence is limited to certain SAT categories and lacks theoretical proof. Furthermore, the impact of structural measures on SAT solvers' behavior has not been extensively studied. This work provides a comprehensive study on structural measures for SAT, including an overview of related works, a taxonomy of measures, and detailed applications in enhancing SAT solvers, generating SAT instances, and classifying SAT instances.

ACM COMPUTING SURVEYS (2023)

Article Computer Science, Artificial Intelligence

An overview of machine learning techniques in constraint solving

Andrei Popescu et al.

Summary: Constraint solving is widely applied in various application contexts, and machine learning can optimize search processes in constraint solving, playing an important role in configuration, recommendation, and model diagnosis.

JOURNAL OF INTELLIGENT INFORMATION SYSTEMS (2022)

Proceedings Paper Computer Science, Artificial Intelligence

Goal-Aware Neural SAT Solver

Emils Ozolins et al.

Summary: In this paper, a query mechanism is proposed to enhance the performance of neural networks in solving SAT problems. By formulating an unsupervised loss function and conducting experiments, it is demonstrated that the proposed approach outperforms the neural baseline.

2022 INTERNATIONAL JOINT CONFERENCE ON NEURAL NETWORKS (IJCNN) (2022)

Review Management

Machine learning for combinatorial optimization: A methodological tour d'horizon

Yoshua Bengio et al.

Summary: This paper surveys recent attempts from the machine learning and operations research communities to leverage machine learning for solving combinatorial optimization problems, advocating for further integration and providing a methodology for doing so. The main point of the paper is to view generic optimization problems as data points to investigate the relevant distribution of problems for learning on a specific task.

EUROPEAN JOURNAL OF OPERATIONAL RESEARCH (2021)

Article Computer Science, Artificial Intelligence

Popularity-similarity random SAT formulas

Jesus Giraldez-Cru et al.

Summary: In the process of solving SAT problems, random SAT instance generators become crucial in explaining the success of algorithms on industrial problems and providing pseudo-industrial random SAT instances with desired properties. This work presents a random SAT instances generator based on the notion of locality, combining both locality and popularity as decisive dimensions of attractiveness among the variables of a formula. This is the first random SAT model that generates both scale-free structure and community structure at once.

ARTIFICIAL INTELLIGENCE (2021)

Article Computer Science, Artificial Intelligence

Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT

Sean B. Holden

Summary: The decision problem for Boolean satisfiability (SAT) is NP-complete, with its quantified version (QSAT) being PSPACE-complete. Despite their computational complexity, methods have been developed to solve large instances within reasonable resources. Machine learning plays a significant role in developing state-of-the-art solvers, but its application requires caution due to potential counterproductivity.

FOUNDATIONS AND TRENDS IN MACHINE LEARNING (2021)

Proceedings Paper Computer Science, Theory & Methods

Deep Cooperation of CDCL and Local Search for SAT

Shaowei Cai et al.

Summary: The study proposes deeper cooperation techniques by enhancing the performance of three typical CDCL solvers, particularly on satisfiable instances. These techniques significantly improve the solver's capabilities and lead to successful outcomes in various benchmarks.

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 (2021)

Article Automation & Control Systems

A Novel Heterogeneous Actor-critic Algorithm with Recent Emphasizing Replay Memory

Bao Xi et al.

Summary: In this paper, an off-policy heterogeneous actor-critic (HAC) algorithm is proposed to improve the training efficiency and performance of reinforcement learning in continuous control tasks by combining soft Q-function and ordinary Q-function; a new sampling technique is introduced to boost policy training and HER is integrated to handle sparse reward tasks; experimental results demonstrate the method's outperformance of prior state-of-the-art methods in terms of training efficiency and performance.

INTERNATIONAL JOURNAL OF AUTOMATION AND COMPUTING (2021)

Proceedings Paper Computer Science, Artificial Intelligence

Employing Machine Learning Models to Solve Uniform Random 3-SAT

Aditya Atkari et al.

DATA COMMUNICATION AND NETWORKS, GUCON 2019 (2020)

Article Computer Science, Information Systems

A branching heuristic for SAT solvers based on complete implication graphs

Fan Xiao et al.

SCIENCE CHINA-INFORMATION SCIENCES (2019)

Proceedings Paper Computer Science, Theory & Methods

Machine Learning-Based Restart Policy for CDCL SAT Solvers

Jia Hui Liang et al.

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018 (2018)

Article Computer Science, Artificial Intelligence

Generating SAT instances with community structure

Jesus Giraldez-Cru et al.

ARTIFICIAL INTELLIGENCE (2016)

Proceedings Paper Computer Science, Theory & Methods

Learning Rate Based Branching Heuristic for SAT Solvers

Jia Hui Liang et al.

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016 (2016)

Review Multidisciplinary Sciences

Deep learning

Yann LeCun et al.

NATURE (2015)

Review Multidisciplinary Sciences

Machine learning: Trends, perspectives, and prospects

M. I. Jordan et al.

SCIENCE (2015)

Proceedings Paper Computer Science, Artificial Intelligence

Evaluating CDCL Variable Scoring Schemes

Armin Biere et al.

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015 (2015)

Proceedings Paper Computer Science, Artificial Intelligence

CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability

Shaowei Cai et al.

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015 (2015)

Article Computer Science, Artificial Intelligence

Algorithm runtime prediction: Methods & evaluation

Frank Hutter et al.

ARTIFICIAL INTELLIGENCE (2014)

Article Computer Science, Artificial Intelligence

SATzilla: Portfolio-based algorithm selection for SAT

Lin Xu et al.

JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH (2008)