On Improving the Backjump Level in PB Solvers

• URL: http://arxiv.org/abs/2107.13085v1
• Date: Tue, 27 Jul 2021 21:23:03 GMT
• Title: On Improving the Backjump Level in PB Solvers
• Authors: Romain Wallon
• Abstract summary: We show that there is no guarantee to perform the highest possible backjump in a SAT solver in the presence of PB constraints. We introduce and evaluate different approaches designed to improve the backjump level identified during conflict analysis. Our experiments show that sub-optimal backjumps are fairly common in PB solvers, even though their impact on the solver is not clear.
• Score: 2.741266294612776
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Current PB solvers implement many techniques inspired by the CDCL architecture of modern SAT solvers, so as to benefit from its practical efficiency. However, they also need to deal with the fact that many of the properties leveraged by this architecture are no longer true when considering PB constraints. In this paper, we focus on one of these properties, namely the optimality of the so-called first unique implication point (1-UIP). While it is well known that learning the first assertive clause produced during conflict analysis ensures to perform the highest possible backjump in a SAT solver, we show that there is no such guarantee in the presence of PB constraints. We also introduce and evaluate different approaches designed to improve the backjump level identified during conflict analysis by allowing to continue the analysis after reaching the 1-UIP. Our experiments show that sub-optimal backjumps are fairly common in PB solvers, even though their impact on the solver is not clear.

Related papers

• Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives [16.101435842520473]
  This paper studies the challenging yet important problem in POMDPs known as the (indefinite-horizon) Maximal Reachability Probability Problem. Inspired by the success of point-based methods developed for discounted problems, we study their extensions to MRPP. We present a novel algorithm that leverages the strengths of these techniques for efficient exploration of the belief space.
  arXiv  Detail & Related papers  (2024-06-05T02:33:50Z)
• Theoretically Achieving Continuous Representation of Oriented Bounding Boxes [64.15627958879053]
  This paper endeavors to completely solve the issue of discontinuity in Oriented Bounding Box representation. We propose a novel representation method called Continuous OBB (COBB) which can be readily integrated into existing detectors. For fairness and transparency of experiments, we have developed a modularized benchmark based on the open-source deep learning framework Jittor's detection toolbox JDet for OOD evaluation.
  arXiv  Detail & Related papers  (2024-02-29T09:27:40Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  The sequential decision-making problem is statistically learnable if it admits a low-rank structure modeled by predictive state representations (PSRs) This paper proposes the first known UCB-type approach for PSRs, featuring a novel bonus term that upper bounds the total variation distance between the estimated and true models. In contrast to existing approaches for PSRs, our UCB-type algorithms enjoy computational tractability, last-iterate guaranteed near-optimal policy, and guaranteed model accuracy.
  arXiv  Detail & Related papers  (2023-07-01T18:35:21Z)
• DeciLS-PBO: an Effective Local Search Method for Pseudo-Boolean Optimization [10.513103815142731]
  We find two ways to improve the local search algorithms in solving Pseudo-Boolean Optimization (PBO) Our algorithm DeciLS-PBO has a promising performance compared to the state-of-the-art algorithms.
  arXiv  Detail & Related papers  (2023-01-28T17:03:56Z)
• Optimizing Two-way Partial AUC with an End-to-end Framework [154.47590401735323]
  Area Under the ROC Curve (AUC) is a crucial metric for machine learning. Recent work shows that the TPAUC is essentially inconsistent with the existing Partial AUC metrics. We present the first trial in this paper to optimize this new metric.
  arXiv  Detail & Related papers  (2022-06-23T12:21:30Z)
• On Dedicated CDCL Strategies for PB Solvers [6.716102421801302]
  We present and evaluate different ways of adapting CDCL strategies to take the specificities of PB constraints into account. Our experiments show that these dedicated strategies allow to improve, sometimes significantly, the performance of these solvers.
  arXiv  Detail & Related papers  (2021-09-02T15:22:27Z)
• Bayesian decision-making under misspecified priors with applications to meta-learning [64.38020203019013]
  Thompson sampling and other sequential decision-making algorithms are popular approaches to tackle explore/exploit trade-offs in contextual bandits. We show that performance degrades gracefully with misspecified priors.
  arXiv  Detail & Related papers  (2021-07-03T23:17:26Z)
• Equilibrium Learning in Combinatorial Auctions: Computing Approximate Bayesian Nash Equilibria via Pseudogradient Dynamics [0.0]
  We present a generic yet scalable alternative multi-agent equilibrium learning method. We observe fast and robust convergence to approximate BNE in a wide variety of auctions.
  arXiv  Detail & Related papers  (2021-01-28T11:53:32Z)
• Combinatorial Pure Exploration with Full-bandit Feedback and Beyond: Solving Combinatorial Optimization under Uncertainty with Limited Observation [70.41056265629815]
  When developing an algorithm for optimization, it is commonly assumed that parameters such as edge weights are exactly known as inputs. In this article, we review recently proposed techniques for pure exploration problems with limited feedback.
  arXiv  Detail & Related papers  (2020-12-31T12:40:52Z)
• Provably Efficient Reward-Agnostic Navigation with Linear Value Iteration [143.43658264904863]
  We show how iteration under a more standard notion of low inherent Bellman error, typically employed in least-square value-style algorithms, can provide strong PAC guarantees on learning a near optimal value function. We present a computationally tractable algorithm for the reward-free setting and show how it can be used to learn a near optimal policy for any (linear) reward function.
  arXiv  Detail & Related papers  (2020-08-18T04:34:21Z)

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.