2
$\begingroup$

Assume a set of variable $V$ = $\{v_1,...,v_m\}$.

Given total $n$ at-most-one (AMO) constraints (at most one element in a given set is true) set [of the below form], over the variable set $V$,

$$ AMO \, (v_1, v_4, \neg v_6, v_{10}) \\ ... \\ AMO \, (v_2, \neg v_3, v_7)$$

Problem: Find an assignment to $V$ that maximize
         the number of satisfiable AMO constraint set. 

I'm unable to represent it as MAX-SAT problem.

Tried so far (Attempt 1): Using hard constraint for each of At-Most-One constraint. This will not work as encoding of $AMO (v_i,...,v_w)$ will have multiple clauses for each $AMO$ and all of them have assigned same weight (top weight). A solution to this set may not be the maximal one.

Attempt (2): To fix the above problem, I tried relative clause weight; i.e., for each clause assign weight proportional to size of the clause. This will give preference of assigning satisfying shorter clause. But this do not work in extreme situations like if all clause have same length.

I have experience with SAT solvers but this is my first MAX-SAT problem attempt.

$\endgroup$

1 Answer 1

3
$\begingroup$

The standard way to create soft constraints in MaxSAT is to use label variables:

For each $AMO_j$ constraint, create a new variable $l_j$. Then create an unit clause $(\lnot l_j)$ with weight $1$ and add the literal $l_j$ to every clause of the standard $AMO_j$ encoding that contains only hard (infinite weight) clauses.

Now the label variable $l_j$ acts as a switch: setting $l_j = true$ will "turn off" the $AMO_j$ hard constraint, but does not satisfy the unit clause $(\lnot l_j)$.

$\endgroup$
5
  • $\begingroup$ Thanks @Laakeri. Yesterday I came up with this hack of using auxiliary variable to achieve this :) Cheers. Is this the best we can do? This adds additional unit clauses of length |#C|, and in conjunction with most effective cardinality encoding of AMO (3n+4 or very close to this number) this will be manageable but big clause set. Excuse if these things are trivial, just started to get my hands on MAX-SAT. Thanks. $\endgroup$
    – Pushpa
    Jan 2, 2020 at 9:17
  • 1
    $\begingroup$ I don't know if this is the best we can do. MaxSAT and IP solvers can be very unpredictable, so the only way to know what is the best solution is to try different things. I would also suggest to try different AMO encodings, the one with the least variables/clauses may not be the best. $\endgroup$
    – Laakeri
    Jan 2, 2020 at 9:57
  • $\begingroup$ Created a chatroom for the discussion: chat.stackexchange.com/rooms/102789/chat-with-pushpa $\endgroup$
    – Laakeri
    Jan 2, 2020 at 10:37
  • $\begingroup$ Is it possible to direct MaxSAT to stop with a cutoff time and return current_max solution. May not be an optimal solution but a solution it finds to be max till this time of the search. Thanks $\endgroup$
    – Pushpa
    Jan 18, 2020 at 18:20
  • 1
    $\begingroup$ Yes, there are MaxSAT solvers that are designed for that. The key word is "Incomplete MaxSAT". $\endgroup$
    – Laakeri
    Jan 18, 2020 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.