Algorithms generate diverse solutions to complex logic problems
On Diverse Solutions to Max-k-CSP and Bounded Degree k-SAT
Data Structures and Algorithms
Summary
Sometimes, it's useful to find many different ways to solve a tricky puzzle where many statements must be true at once. This paper studies how to find multiple solutions that are not only good at solving the puzzle but also quite different from each other according to two ways of measuring difference. The researchers developed efficient methods to create sets of solutions that balance being correct and diverse. They also showed some problems of measuring exact diversity are hard to solve but provided ways to find approximate diverse solutions efficiently.
What this means in practice
- •For software debugging teams: Generate multiple varied solutions to identify diverse error scenarios during program verification and debugging involving logical constraints.
- •For cryptography engineers: Produce diverse approximate solutions in high-dimensional logical spaces to enhance testing of cryptographic protocols under multiple configurations.
Authors
Mayank Goswami, Adarsh Srinivasan
Abstract
We study the problem of generating diverse solutions to Max-$k$-CSP and bounded-degree $k$-SAT, focusing on two distinct metrics: constraint diversity and variable diversity. For constraint diversity, the goal is to output $s \geq 2$ assignments to the CSP such that each assignment satisfies a $c$-fraction of the constraints, while maximizing the diversity among the $0$-$1$ indicator vectors of satisfied constraints in the Hamming metric. By reducing this to a multi-criteria optimization problem, we design $poly(n,s)$ time approximation algorithms that return s assignments achieving provable bi-criteria guarantees on both the fraction of satisfied constraints and diversity of the constraint vectors. For variable diversity, the objective is to maximize the Hamming distance between the assignments, while also maximizing the number of constraints satisfied. For Max-$k$-CSP instances when the desired number of solutions is $s=2^{O(n)}$, we implicitly represent these diverse approximate solutions by constructing linear codes within the solution space. Finally, we investigate variable diversity for $k$-SAT in the Lovász Local Lemma regime. In this setting, we establish NP-hardness for the exact diversity problem (computing the diameter of the solution space) and provide a polynomial-time approximation algorithm to efficiently generate diverse satisfying assignments.