Improving probability selecting based weights for Satisfiability Problem
- URL: http://arxiv.org/abs/2007.15185v1
- Date: Thu, 30 Jul 2020 02:23:07 GMT
- Title: Improving probability selecting based weights for Satisfiability Problem
- Authors: Huimin Fu, Yang Xu, Jun Liu, Guanfeng Wu, Sutcliffe Geoff
- Abstract summary: We present a new SLS algorithm named SelectNTS for uniform random k-SAT and HRS.
Our algorithm outperforms state-of-the-art random SAT algorithms, and our SelectNTS can effectively solve both uniform random k-SAT and HRS.
- Score: 6.59413630027528
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The Boolean Satisfiability problem (SAT) is important on artificial
intelligence community and the impact of its solving on complex problems.
Recently, great breakthroughs have been made respectively on stochastic local
search (SLS) algorithms for uniform random k-SAT resulting in several
state-of-the-art SLS algorithms Score2SAT, YalSAT, ProbSAT, CScoreSAT and on a
hybrid algorithm for hard random SAT (HRS) resulting in one state-of-the-art
hybrid algorithm SparrowToRiss. However, there is no an algorithm which can
effectively solve both uniform random k-SAT and HRS. In this paper, we present
a new SLS algorithm named SelectNTS for uniform random k-SAT and HRS. SelectNTS
is an improved probability selecting based local search algorithm for SAT
problem. The core of SelectNTS relies on new clause and variable selection
heuristics. The new clause selection heuristic uses a new clause weighting
scheme and a biased random walk. The new variable selection heuristic uses a
probability selecting strategy with the variation of CC strategy based on a new
variable weighting scheme. Extensive experimental results on the well-known
random benchmarks instances from the SAT Competitions in 2017 and 2018, and on
randomly generated problems, show that our algorithm outperforms
state-of-the-art random SAT algorithms, and our SelectNTS can effectively solve
both uniform random k-SAT and HRS.
Related papers
- General Method for Solving Four Types of SAT Problems [12.28597116379225]
Existing methods provide varying algorithms for different types of Boolean satisfiability problems (SAT)
This study proposes a unified framework DCSAT based on integer programming and reinforcement learning (RL) algorithm to solve different types of SAT problems.
arXiv Detail & Related papers (2023-12-27T06:09:48Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
We introduce the notion of decomposition hardness (d-hardness)
We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
arXiv Detail & Related papers (2023-12-16T12:44:36Z) - Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments.
Experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.
arXiv Detail & Related papers (2023-04-18T05:33:33Z) - HARRIS: Hybrid Ranking and Regression Forests for Algorithm Selection [75.84584400866254]
We propose a new algorithm selector leveraging special forests, combining the strengths of both approaches while alleviating their weaknesses.
HARRIS' decisions are based on a forest model, whose trees are created based on optimized on a hybrid ranking and regression loss function.
arXiv Detail & Related papers (2022-10-31T14:06:11Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning.
The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
arXiv Detail & Related papers (2022-10-04T09:19:13Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem.
DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions.
arXiv Detail & Related papers (2022-05-27T03:20:42Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems.
In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
arXiv Detail & Related papers (2021-07-15T04:47:35Z) - diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT
and Answer Set Programming [0.0]
diff-SAT combines regular solving with the capability to use probabilistic clauses, facts and rules.
The sampling process minimizes a user-defined differentiable objective function.
arXiv Detail & Related papers (2021-01-03T09:04:31Z) - Optimal Randomized First-Order Methods for Least-Squares Problems [56.05635751529922]
This class of algorithms encompasses several randomized methods among the fastest solvers for least-squares problems.
We focus on two classical embeddings, namely, Gaussian projections and subsampled Hadamard transforms.
Our resulting algorithm yields the best complexity known for solving least-squares problems with no condition number dependence.
arXiv Detail & Related papers (2020-02-21T17:45:32Z) - Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms.
We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
arXiv Detail & Related papers (2020-01-29T09:40:58Z) - NLocalSAT: Boosting Local Search with Solution Prediction [36.69915361918781]
An effective way for solving a satisfiable SAT problem is the local search (SLS)
This method is assigned in a random manner, which impacts the effectiveness of SLS solvers.
NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network.
Experiments show that solvers with NLocalSAT achieve 27% 62% improvement over the original SLS solvers.
arXiv Detail & Related papers (2020-01-26T04:22:53Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.