Related papers: MaxSAT Resolution and Subcube Sums
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear…
In this paper we prove lower bounds for sizes of refutations of unsatisfiable vector Subset Sum instances $\overrightarrow{a}_1 x_1 + \dots + \overrightarrow{a}_n x_n = \overrightarrow{b}$ in the proof system Res(lin$_{\mathbb{F}_q}$) where…
We consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like…
MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the last decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have…
We consider semidefinite programming (SDP) approaches for solving the maximum satisfiability problem (MAX-SAT) and the weighted partial MAX-SAT. It is widely known that SDP is well-suited to approximate the (MAX-)2-SAT. Our work shows the…
In this paper we study an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations…
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et$.$al'20,…
Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately,…
Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually,…
Machine learning systems have been extensively used as auxiliary tools in domains that require critical decision-making, such as healthcare and criminal justice. The explainability of decisions is crucial for users to develop trust on these…
Random constraint satisfaction problems (CSPs) such as random $3$-SAT are conjectured to be computationally intractable. The average case hardness of random $3$-SAT and other CSPs has broad and far-reaching implications on problems in…
We introduce a new method for building higher-degree sum-of-squares lower bounds over the hypercube $\mathbf{x} \in \{\pm 1\}^N$ from a given degree 2 lower bound. Our method constructs pseudoexpectations that are positive semidefinite by…
Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs…
We introduce an extended tableau calculus for answer set programming (ASP). The proof system is based on the ASP tableaux defined in [Gebser&Schaub, ICLP 2006], with an added extension rule. We investigate the power of Extended ASP Tableaux…
The objective of this paper is to develop simple techniques to bound the optimal uplink sum-rate of multi-user RIS-aided wireless systems. Specifically, we develop a novel technique called \textit{channel separation} which provides a new…
The optimization version of the cavity method for single instances, called Max-Sum, has been applied in the past to the Minimum Steiner Tree Problem on Graphs and variants. Max-Sum has been shown experimentally to give asymptotically…
Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of the unsatisfied soft clauses without providing any optimality guarantees. In this paper, we propose two approximation strategies…
We introduce a method for proving lower bounds on the efficacy of semidefinite programming (SDP) relaxations for combinatorial problems. In particular, we show that the cut, TSP, and stable set polytopes on $n$-vertex graphs are not the…
The Stabbing Planes proof system was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas --…
Maximum Satisfiability (MaxSAT) is an optimization variant of the Boolean Satisfiability (SAT) problem. In general, MaxSAT algorithms perform a succession of SAT solver calls to reach an optimum solution making extensive use of cardinality…