0
$\begingroup$

MaxSAT is a problem related to SAT where there is a finite collection of hard and soft clauses which share boolean variables. The hard clauses must be satisfied while the soft clauses have a weight. The sum of weights of the satisfied clauses is to be maximized.

Multi-Objective Max-SAT is generalization where soft clauses have multiple weights which count towards different objectives. The optima is therefor often not a single assignment but a set of points that show the tradeoff between the objectives. For $n+1$ linearly independent objectives one expects an "$n$ dimensional manifold" as paretofront, the set of points that are not dominated by other points. Max-SAT problems by their nature have a discrete and finite space of possible objective values.

$x^*$ domaninates $y$ in maximization problem if and only iff for all $n$ objectives:

$$ (f_1(y) <= f_1(x^*) \land f_2(y) <= f_2(x^*) \land \ ... \ \land f_n(y) <= f_n(x^*) ) \land (f_1(y) + f_2(y) + \ ... \ + f_n(y) < f_1(x^*) + f_2(x^*) + \ ... \ + f_n(x^*) ) $$

The MaxHS Algorithm for MaxSAT works as follows:

Require: P=(p, L, c) an equivalent minimization problem 
Ensure: returns S ∈ Solc(P) if Sol(P)!=∅, and other-wise “no solution”

  K:=∅;
  while not(∅ ∈ K) do 
    let S be s.t. S ∈ minimumcostHS(c,K);
    if p(S) then return S;
    K := union(K,{extractcore(S)});
  return “no solution”;

where L is the finite set of variables occurring in the soft clauses, p a predicate over $2^L$ which checks whether the hard clauses are satisfiable under this partial assignment, and c: $L→R^+$ the cost of this partial assignment. The algorithm is described in more detail here.

Seeing how a SAT solver is used as oracle to see whether a choice of variables occurring in the soft clauses is viable and learn more about the problem using cores produced by the SAT attempt in case of failure. It stands to reason that a slight modification of the algorithm can produce the pareto frontier of an multi-objective SAT problem.

Such as:

Require: P=(p, L, c) a minimization problem 
Ensure: returns S ∈ Solc(P) if Sol(P)!=∅, and other-wise “no solution”
  PF:=∅;
  K:=∅;
  while not(∅ ∈ K) do 
    let S be s.t. S ∈ minimumcostHS(c,K);
    if p(S) then 
      PF := union(PF,{S});
      accept(S);
    else
      K := union(K,{extractcore(S)});
  return PF;

where L is finite set, p a predicate over $2^L$, and c: $L→(R^+)^n$.

This requires additional modifications of minumumcostHS such that it's aware of the pareto nature of the problem and that it doesn't have to search for solution which would be dominated by something that is already accepted (using this mechanism one could also exclude assignments that are equal in all objectives to something known).

Do you have any suggestions what algorithm i could use for minumumcostHS and accept to complete the algorithm such that it finds one assignment for all objective combinations that are part of the pareto set?

minimumcostHS for MaxSAT is implemented using Integer linear programming.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.