Optimal stopping methods for finding high quality solutions to satisfiability problems with preferences

Satisfiability problems with preferences enrich the expressive power of the Boolean Satisfiability problem (SAT) and facilitate the representation of qualitative/quantitative preferences on literals/formulas, defining an optimization problem. In some cases, it is not strictly necessary to compute an optimal solution, but it is enough to compute a sub-optimal solution of high quality and, possibly, provide a lower bound on the probability of finding an optimal solution. The 1/e - rule is the optimal stopping rule for the secretary problem that guarantees an optimal solution with probability at least 1/e can be found. In this paper: we show how to apply the 1/e-rule for solving satisfiability problems with preferences; we show that its theoretical success rate of about 37% is greater than 90% on random benchmarks; and, we show that the performance of the 1/e-rule on structured benchmarks is sometimes many orders-of-magnitude worse than that of complete search-based algorithms, and we explain the reasons why. We propose an algorithm based on the idea underlying the 1/e-rule, which needs the generation of just two solutions: the experimental evaluation shows that the average success rate of the proposed algorithm is a good approximation of the theoretical one of the 1/e-rule, since it is about 50.92% on 1956 structured problems and 48.33% on 2400 randomly generated instances with 200 variables.