Adversarial Satisfiability Problem

TL;DR

This paper investigates the adversarial satisfiability problem where an adversary manipulates variable negations to make formulas unsatisfiable, revealing that optimal strategies are nearly balanced and highlighting complex finite-size effects.

Contribution

It introduces the adversarial satisfiability problem, applies the cavity method to analyze large deviations, and uncovers near-optimal adversarial strategies and finite-size effects.

Findings

Optimal adversarial strategy balances negations per variable.

Large deviations of entropy are computed using the cavity method.

Strong pre-asymptotic effects are observed in small instances.

Abstract

We study the adversarial satisfiability problem, where the adversary can choose whether variables are negated in clauses or not in order to make the resulting formula unsatisfiable. This is one case of a general class of adversarial optimization problems that often arise in practice and are algorithmically much harder than the standard optimization problems. We use the cavity method to compute large deviations of the entropy in the random satisfiability problem with respect to the negation-configurations. We conclude that in the thermodynamic limit the best strategy the adversary can adopt is extremely close to simply balancing the number of times every variable is and is not negated. We also conduct a numerical study of the problem, and find that there are very strong pre-asymptotic effects that are due to the fact that for small sizes exponential and factorial growth is hardly distinguishable.