HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

• URL: http://arxiv.org/abs/2302.02104v3
• Date: Thu, 8 Feb 2024 13:49:57 GMT
• Title: HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline
• Authors: Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Wanqian Luo, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Junchi Yan
• Abstract summary: Existing SAT generation approaches can hardly simultaneously capture the global structural properties and maintain plausible computational hardness. We propose HardSATGEN, which introduces a fine-grained control mechanism to the neural split-merge paradigm for SAT formula generation. Compared to the best previous methods, the average performance gains achieve 38.5% in structural statistics, 88.4% in computational metrics, and over 140.7% in the effectiveness of guiding solver tuning.
• Score: 45.91245228386502
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Industrial SAT formula generation is a critical yet challenging task. Existing SAT generation approaches can hardly simultaneously capture the global structural properties and maintain plausible computational hardness. We first present an in-depth analysis for the limitation of previous learning methods in reproducing the computational hardness of original instances, which may stem from the inherent homogeneity in their adopted split-merge procedure. On top of the observations that industrial formulae exhibit clear community structure and oversplit substructures lead to the difficulty in semantic formation of logical structures, we propose HardSATGEN, which introduces a fine-grained control mechanism to the neural split-merge paradigm for SAT formula generation to better recover the structural and computational properties of the industrial benchmarks. Experiments including evaluations on private and practical corporate testbed show the superiority of HardSATGEN being the only method to successfully augment formulae maintaining similar computational hardness and capturing the global structural properties simultaneously. Compared to the best previous methods, the average performance gains achieve 38.5% in structural statistics, 88.4% in computational metrics, and over 140.7% in the effectiveness of guiding solver tuning by our generated instances. Source code is available at http://github.com/Thinklab-SJTU/HardSATGEN

Related papers

• ZeroLM: Data-Free Transformer Architecture Search for Language Models [54.83882149157548]
  Current automated proxy discovery approaches suffer from extended search times, susceptibility to data overfitting, and structural complexity. This paper introduces a novel zero-cost proxy methodology that quantifies model capacity through efficient weight statistics. Our evaluation demonstrates the superiority of this approach, achieving a Spearman's rho of 0.76 and Kendall's tau of 0.53 on the FlexiBERT benchmark.
  arXiv  Detail & Related papers  (2025-03-24T13:11:22Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  We introduce PromptCoT, a novel approach for automatically generating high-quality Olympiad-level math problems. The proposed method synthesizes complex problems based on mathematical concepts and the rationale behind problem construction. Our method is evaluated on standard benchmarks including GSM8K, MATH-500, and AIME2024, where it consistently outperforms existing problem generation methods.
  arXiv  Detail & Related papers  (2025-03-04T06:32:30Z)
• Assisting Mathematical Formalization with A Learning-based Premise Retriever [29.06255449960557]
  We introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• The Power of Resets in Online Reinforcement Learning [73.64852266145387]
  We explore the power of simulators through online reinforcement learning with local simulator access (or, local planning) We show that MDPs with low coverability can be learned in a sample-efficient fashion with only $Qstar$-realizability. We show that the notorious Exogenous Block MDP problem is tractable under local simulator access.
  arXiv  Detail & Related papers  (2024-04-23T18:09:53Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers.
  arXiv  Detail & Related papers  (2023-09-20T16:27:52Z)
• Structured Sentiment Analysis as Transition-based Dependency Parsing [0.40611352512781856]
  Structured sentiment analysis aims to automatically extract people's opinions from a text in natural language. One of the most accurate methods for performing SSA was recently proposed and consists of approaching it as a dependency parsing task. We present the first transition-based method to address SSA as dependency parsing.
  arXiv  Detail & Related papers  (2023-05-09T10:03:34Z)
• Principled and Efficient Motif Finding for Structure Learning of Lifted Graphical Models [5.317624228510748]
  Structure learning is a core problem in AI central to the fields of neuro-symbolic AI and statistical relational learning. We present the first principled approach for mining structural motifs in lifted graphical models. We show that we outperform state-of-the-art structure learning approaches by up to 6% in terms of accuracy and up to 80% in terms of runtime.
  arXiv  Detail & Related papers  (2023-02-09T12:21:55Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  W2SAT is a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances. We introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability. Decoding from WLIG into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method.
  arXiv  Detail & Related papers  (2023-02-01T06:30:41Z)
• Amortized Inference for Causal Structure Learning [72.84105256353801]
  Learning causal structure poses a search problem that typically involves evaluating structures using a score or independence test. We train a variational inference model to predict the causal structure from observational/interventional data. Our models exhibit robust generalization capabilities under substantial distribution shift.
  arXiv  Detail & Related papers  (2022-05-25T17:37:08Z)
• Symbolic Regression by Exhaustive Search: Reducing the Search Space Using Syntactical Constraints and Efficient Semantic Structure Deduplication [2.055204980188575]
  Symbolic regression is a powerful system identification technique in industrial scenarios where no prior knowledge on model structure is available. In this chapter we introduce a deterministic symbolic regression algorithm specifically designed to address these issues. A finite enumeration of all possible models is guaranteed by structural restrictions as well as a caching mechanism for detecting semantically equivalent solutions.
  arXiv  Detail & Related papers  (2021-09-28T17:47:51Z)
• RANK-NOSH: Efficient Predictor-Based Architecture Search via Non-Uniform Successive Halving [74.61723678821049]
  We propose NOn-uniform Successive Halving (NOSH), a hierarchical scheduling algorithm that terminates the training of underperforming architectures early to avoid wasting budget. We formulate predictor-based architecture search as learning to rank with pairwise comparisons. The resulting method - RANK-NOSH, reduces the search budget by 5x while achieving competitive or even better performance than previous state-of-the-art predictor-based methods on various spaces and datasets.
  arXiv  Detail & Related papers  (2021-08-18T07:45:21Z)
• 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)
• Efficient Micro-Structured Weight Unification and Pruning for Neural Network Compression [56.83861738731913]
  Deep Neural Network (DNN) models are essential for practical applications, especially for resource limited devices. Previous unstructured or structured weight pruning methods can hardly truly accelerate inference. We propose a generalized weight unification framework at a hardware compatible micro-structured level to achieve high amount of compression and acceleration.
  arXiv  Detail & Related papers  (2021-06-15T17:22:59Z)

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.