|
| | | | |
| | | |
| Stat |
Members: 3662
Articles: 2'599'751
Articles rated: 2609
13 December 2024 |
|
| | | | |
|
Article overview
| |
|
|
W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs | | Weihuang Wen
; Tianshu Yu
; | | Date: |
1 Feb 2023 | | Abstract: | The Boolean Satisfiability (SAT) problem stands out as an attractive
NP-complete problem in theoretic computer science and plays a central role in a
broad spectrum of computing-related applications. Exploiting and tuning SAT
solvers under numerous scenarios require massive high-quality industry-level
SAT instances, which unfortunately are quite limited in the real world. To
address the data insufficiency issue, in this paper, we propose W2SAT, a
framework to generate SAT formulas by learning intrinsic structures and
properties from given real-world/industrial instances in an implicit fashion.
To this end, we introduce a novel SAT representation called Weighted Literal
Incidence Graph (WLIG), which exhibits strong representation ability and
generalizability against existing counterparts, and can be efficiently
generated via a specialized learning-based graph generative model. Decoding
from WLIGs into SAT problems is then modeled as finding overlapping cliques
with a novel hill-climbing optimization method termed Optimal Weight Coverage
(OWC). Experiments demonstrate the superiority of our WLIG-induced approach in
terms of graph metrics, efficiency, and scalability in comparison to previous
methods. Additionally, we discuss the limitations of graph-based SAT generation
for real-world applications, especially when utilizing generated instances for
SAT solver parameter-tuning, and pose some potential directions. | | Source: | arXiv, 2302.00272 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|
REGISTER