SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning

• URL: http://arxiv.org/abs/2411.02035v1
• Date: Mon, 04 Nov 2024 12:37:59 GMT
• Title: SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning
• Authors: Gaspard Quenard, Damier Pellier, Humbert Fiorino,
• Abstract summary: This paper presents SibylSat, a novel SAT-based method designed to efficiently solve totally-ordered HTN problems (TOHTN) In contrast to prevailing SAT-based HTN planners that employ a breadth-first search strategy, SibylSat adopts a greedy search approach, enabling it to identify promising decompositions for expansion. Our experimental evaluations demonstrate that SibylSat outperforms existing SAT-based TOHTN approaches in terms of both runtime and plan quality on most of the IPC benchmarks.
• Score: 2.2276906461400054
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper presents SibylSat, a novel SAT-based method designed to efficiently solve totally-ordered HTN problems (TOHTN). In contrast to prevailing SAT-based HTN planners that employ a breadth-first search strategy, SibylSat adopts a greedy search approach, enabling it to identify promising decompositions for expansion. The selection process is facilitated by a heuristic derived from solving a relaxed problem, which is also expressed as a SAT problem. Our experimental evaluations demonstrate that SibylSat outperforms existing SAT-based TOHTN approaches in terms of both runtime and plan quality on most of the IPC benchmarks, while also solving a larger number of problems.

Related papers

• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
  The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering. This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically.
  arXiv  Detail & Related papers  (2025-02-20T07:25:21Z)
• Deeply Optimizing the SAT Solver for the IC3 Algorithm [0.23749905164931204]
  We introduce several optimizations for the SAT solver in IC3 based on our observations. We replace the binary heap with buckets to achieve constant-time operations. We develop a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations.
  arXiv  Detail & Related papers  (2025-01-24T12:40:43Z)
• Training Greedy Policy for Proposal Batch Selection in Expensive Multi-Objective Combinatorial Optimization [52.80408805368928]
  We introduce a novel greedy-style subset selection algorithm for batch acquisition. Our experiments on the red fluorescent proteins show that our proposed method achieves the baseline performance in 1.69x fewer queries.
  arXiv  Detail & Related papers  (2024-06-21T05:57:08Z)
• 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)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
  arXiv  Detail & Related papers  (2023-06-07T12:19:22Z)
• Evolutionary Diversity Optimisation in Constructing Satisfying Assignments [20.386139395296215]
  This paper studies the Boolean satisfiability problem (SAT) in the context of EDO. SAT is of great importance in computer science and differs from the other problems studied in EDO literature, such as KP and TSP. We introduce evolutionary algorithms employing a well-known SAT solver to maximise diversity among a set of SAT solutions explicitly.
  arXiv  Detail & Related papers  (2023-05-19T06:26:10Z)
• 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)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  This paper introduces SATformer, a Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.
  arXiv  Detail & Related papers  (2022-09-02T11:17:39Z)
• 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)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• 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)
• 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.