ABSTRACT. Local search (LS) is an efficient method for solving combinatorial optimization problems such as MaxSAT and Pseudo Boolean Problems (PBO). But due to the lack of reasoning power and global information, LS methods get stuck at local optima easily. In contrast, systematic search utilize unit propagation and clause learning techniques with strong reasoning power to avoid falling into local optima. However, the complete search is generally time-consuming. This work proposes a deep cooperation framework of local search and unit propagation to address their inherent disadvantages. First, we design a mechanism to observe the stuck situation of the LS, and then a well designed unit propagation procedure is called to help get out of the local optima. Experiments based on MaxSAT Evaluations, PBO competition , the Mixed Integer Programming Library and real-life cases validate that our method can bring huge improvements in state-of-the-art MaxSAT and PBO LS solvers.

ABSTRACT. In facility location problems we seek to locate a set of facilities so that some criterion is optimized. In the p-center problem we minimize the maximum distance between clients and their closest facilities, whereas in p-dispersion we maximize the minimum distance between facilities. Recently, a variant of p-dispersion with distance constraints between facilities was studied, and an incomplete CP solver that heuristically prunes branches was shown to be faster than Gurobi and OR-Tools, but often failed to discover optimal/near-optimal solutions. We enhance this work in two directions, regarding effectiveness and applicability. We first show how local search can be used to achieve more focused branch pruning with little extra cost, resulting in optimal or near-optimal solutions being discovered in many more instances. Then, we demonstrate how the framework can be applied on the p-center problem with distance constraints, comparing it to ILP and CP models implemented in Gurobi and OR-Tools.

ABSTRACT. We examine the complexity of maximising fitness via local search on valued constraint satisfaction problems (VCSPs). We consider two kinds of local ascents: (1) steepest ascents, where each step changes the domain that produces a maximal increase in fitness; and(2) $\prec$-ordered ascents, where -- of the domains with available fitness increasing changes -- each step changes the $\prec$-minimal domain. We provide a general padding argument to simulate any ordered ascent by a steepest ascent. We construct a VCSP that is a path of binary constraints between alternating 2-state and 3-state domains with exponentially long ordered ascents. We apply our padding argument to this VCSP to obtain a Boolean VCSP that has a constraint (hyper)graph of arity 5 and pathwidth 4 with exponential steepest ascents. This is an improvement on the previous best known construction for long steepest ascents, which had arity 8 and pathwidth 7.

ABSTRACT. We give a polynomial time algorithm that solves CSP(Z;≤,x=y+1,x=2y), a CSP whose computational complexity was posed as an open question and important substep in classifying the complexity of CSP(Γ) for first-order reducts Γ from (Z,<,+,1). The algorithm works by first reducing the infinite domain to a finite domain by inferring an upper bound on the size of the smallest solution, then repeatedly merging consecutive constraints into new constraints, and finally solving the problem using arc consistency. The algorithm generalizes to CSPs involving relations of the form x ≤ c^a y + b or c^a x + b ≤ y where x and y are variables, a and b are parameters, and c is some fixed constant.

ABSTRACT. Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice.

In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.

ABSTRACT. The \emph{constraint satisfaction problem} asks to decide if a set of constraints over a relational structure $\mathcal{A}$ is satisfiable (CSP$(\mathcal{A})$). We consider CSP$(\mathcal{A} \cup \mathcal{B})$ where $\mathcal{A}$ is a structure and $\mathcal{B}$ is an \emph{alien} structure, and analyse its (parameterized) complexity when at most $k$ alien constraints are allowed. We establish connections and obtain transferable complexity results to several well-studied problems that previously escaped classification attempts. Our novel approach, utilizing logical and algebraic methods, yields an \textsf{FPT} versus \textsf{pNP} dichotomy for arbitrary finite structures and sharper dichotomies for Boolean structures and first-order reducts of $(\mathbb{N},=)$ (equality CSPs), together with many partial results for general $\omega$-categorical structures.

ABSTRACT. Envy-freeness up to any good (EFX) is a key concept in Computational Social Choice for the fair division of indivisible goods, where no agent envies another's allocation after removing any single item. A deeper understanding of EFX allocations is facilitated by exploring the rainbow cycle number ($R_f(d)$), the largest number of independent sets in a certain class of directed graphs. Upper bounds on $R_f(d)$ provide guarantees the feasibility of EFX allocations (Chaudhury et al., EC 2021).

In this work, we precisely compute the numbers $R_f(d)$ for small values of d, employing the SAT modulo Symmetries framework. SAT modulo Symmetries is specifically tailored for the constraint-based isomorph-free generation of combinatorial structures. We provide an efficient encoding for the rainbow cycle number, comparing eager and lazy approaches. To cope with the huge search space, we extend the encoding with invariant pruning, a new method that significantly speeds up computation.

ABSTRACT. This paper presents a SAT encoding, called vertex elimination encoding (VEE), for the Hamiltonian Cycle Problem (HCP). The encoding maps a Hamiltonian cycle in the reduced graph after vertex elimination to a Hamiltonian cycle in the original graph. While VEE is not competitive for large dense graphs due to its large encoding sizes, it can be utilized to reduce graphs when they are sparse. This paper compares VEE with the distance encoding, and shows that the hybridization of these two encodings is effective for the benchmarks. For the knight's tour problem, in particular, the hybrid encoding solves some middle-sized instances that were beyond the reach for previous eager SAT encodings.

ABSTRACT. Weighted model counting (WMC) plays a central role in probabilistic reasoning. Given that this problem is #P-hard, harder instances can generally only be addressed using approximate techniques based on sampling, which provide statistical convergence guarantees: the longer a sampling process runs, the more accurate the WMC is likely to be. In this work, we propose a deterministic search-based approach that can also be stopped at any time and provides hard lower- and upper-bound guarantees on the true WMC. This approach uses a value heuristic that guides exploration first towards models with a high weight and leverages Limited Discrepancy Search to make the bounds converge faster. The validity, scalability, and convergence of our approach are tested and compared with state-of-the-art baseline methods on the problem of computing marginal probabilities in Bayesian networks and reliability estimation in probabilistic graphs.

ABSTRACT. Solution counting and solution space integration over linear constraints are important problems with many applications. Previous works addressed either only counting integer points in polytopes (integer counting) with integer variables or alternatively only computing the volume of polytopes (solution space integration) on variables over the reals, including approximating the integer count via polytope's volume. We are not aware of a non-trivial algorithm which addresses the mixed case, where linear constraints are over mixed integer and real variables. In this paper, we propose a new randomized algorithm to approximate guarantees (bounds) of integer solution counts. Then we present upper and lower bounds for solution space integration over mixed-integer linear constraints. Thus, proposed algorithms can be extended to mixed-integer cases as well. The experiments show that approximations are often very close to exact results in practice, and bounds approximated by our algorithm are often tight and useful.