Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection

• URL: http://arxiv.org/abs/2003.00409v2
• Date: Wed, 4 Mar 2020 03:01:35 GMT
• Title: Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
• Authors: Haokun Li and Bican Xia
• Abstract summary: algorithm for deciding satisfiability of formulas over the reals is proposed. Key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search.
• Score: 0.8702432681310401
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.

Related papers

• A Sample Efficient Alternating Minimization-based Algorithm For Robust Phase Retrieval [56.67706781191521]
  In this work, we present a robust phase retrieval problem where the task is to recover an unknown signal. Our proposed oracle avoids the need for computationally spectral descent, using a simple gradient step and outliers.
  arXiv  Detail & Related papers  (2024-09-07T06:37:23Z)
• Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
  Single-Index Models are high-dimensional regression problems with planted structure. We show that computationally efficient algorithms, both within the Statistical Query (SQ) and the Low-Degree Polynomial (LDP) framework, necessarily require $Omega(dkstar/2)$ samples.
  arXiv  Detail & Related papers  (2024-03-08T18:50:19Z)
• Neural Lattice Reduction: A Self-Supervised Geometric Deep Learning Approach [12.679411410749521]
  We show that it is possible to parametrize the algorithm space for lattice reduction problem with neural networks and find an algorithm without supervised data. We design a deep neural model outputting factorized unimodular matrices and train it in a self-supervised manner by penalizing non-orthogonal lattice bases. We show that this approach yields an algorithm with comparable complexity and performance to the Lenstra-Lenstra-Lov'asz algorithm on a set of benchmarks.
  arXiv  Detail & Related papers  (2023-11-14T13:54:35Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• An Efficient Algorithm for Clustered Multi-Task Compressive Sensing [60.70532293880842]
  Clustered multi-task compressive sensing is a hierarchical model that solves multiple compressive sensing tasks. The existing inference algorithm for this model is computationally expensive and does not scale well in high dimensions. We propose a new algorithm that substantially accelerates model inference by avoiding the need to explicitly compute these covariance matrices.
  arXiv  Detail & Related papers  (2023-09-30T15:57:14Z)
• Best-Subset Selection in Generalized Linear Models: A Fast and Consistent Algorithm via Splicing Technique [0.6338047104436422]
  Best subset section has been widely regarded as the Holy Grail of problems of this type. We proposed and illustrated an algorithm for best subset recovery in mild conditions. Our implementation achieves approximately a fourfold speedup compared to popular variable selection toolkits.
  arXiv  Detail & Related papers  (2023-08-01T03:11:31Z)
• Factorization of Multi-Agent Sampling-Based Motion Planning [72.42734061131569]
  Modern robotics often involves multiple embodied agents operating within a shared environment. Standard sampling-based algorithms can be used to search for solutions in the robots' joint space. We integrate the concept of factorization into sampling-based algorithms, which requires only minimal modifications to existing methods. We present a general implementation of a factorized SBA, derive an analytical gain in terms of sample complexity for PRM*, and showcase empirical results for RRG.
  arXiv  Detail & Related papers  (2023-04-01T15:50:18Z)
• Alternatives to a nonhomogeneous partial differential equation quantum algorithm [52.77024349608834]
  We propose a quantum algorithm for solving nonhomogeneous linear partial differential equations of the form $Apsi(textbfr)=f(textbfr)$. These achievements enable easier experimental implementation of the quantum algorithm based on nowadays technology.
  arXiv  Detail & Related papers  (2022-05-11T14:29:39Z)
• Matrix Reordering for Noisy Disordered Matrices: Optimality and Computationally Efficient Algorithms [9.245687221460654]
  Motivated by applications in single-cell biology and metagenomics, we investigate the problem of matrixing based on a noisy monotone Toeplitz matrix model. We establish fundamental statistical limit for this problem in a decision-theoretic framework and demonstrate that a constrained least squares rate. To address this, we propose a novel-time adaptive sorting algorithm with guaranteed performance improvement.
  arXiv  Detail & Related papers  (2022-01-17T14:53:52Z)
• Minimal Cycle Representatives in Persistent Homology using Linear Programming: an Empirical Study with User's Guide [4.46514714749204]
  Cycle representatives of persistent homology classes can be used to provide descriptions of topological features in data. One approach to solving this problem is to optimize the choice of representative against some measure that is meaningful in the context of the data.
  arXiv  Detail & Related papers  (2021-05-14T18:38:48Z)
• Sparse PCA via $l_{2,p}$-Norm Regularization for Unsupervised Feature Selection [138.97647716793333]
  We propose a simple and efficient unsupervised feature selection method, by combining reconstruction error with $l_2,p$-norm regularization. We present an efficient optimization algorithm to solve the proposed unsupervised model, and analyse the convergence and computational complexity of the algorithm theoretically.
  arXiv  Detail & Related papers  (2020-12-29T04:08:38Z)
• A global-local neighborhood search algorithm and tabu search for flexible job shop scheduling problem [3.946442574906068]
  This work presents a new meta-heuristic algorithm called GLNSA (Global-local neighborhood search algorithm) The proposed algorithm is complemented with a tabu search that implements a simplified version of the Nopt1 neighborhood. Experiments carried out show a satisfactory performance of the proposed algorithm, compared with other results published in recent algorithms.
  arXiv  Detail & Related papers  (2020-10-23T23:08:51Z)
• Solution Path Algorithm for Twin Multi-class Support Vector Machine [6.97711662470035]
  The paper is devoted to the fast regularization parameter tuning algorithm for the twin multi-class support vector machine. A new sample dataset division method is adopted and the Lagrangian multipliers are proved to be piecewise linear. The proposed method can achieve good classification performance with reducing the computational cost of grid search method from exponential level to the constant level.
  arXiv  Detail & Related papers  (2020-05-30T14:05:46Z)

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.