Max Satisfiability Problem

Overview

maximize (c1+2*c2+3*c3+4*c4)
s.t.     c1 = x0 or x1
         c2 = x0 or not x1
         c3 = not x0 or x1
         c4 = not x0 or not x1
         x0, x1 is Binary

This optimization problem is a kind of the weighted MAX-SAT problem. This problem can be formulated using flopt as follows,

import flopt

# literals
x0 = flopt.Variable("x0", cat="Binary")
x1 = flopt.Variable("x1", cat="Binary")

# clauses
c1 = x0 | x1
c2 = x0 | ~x1
c3 = ~x0 | x1
c4 = ~x0 | ~x1

clauses = [c1, c2, c3, c4]
weights = [1, 2, 3, 4]
obj = flopt.dot(clauses, weights)

prob = flopt.Problem("MaxSat", sense="Maximize")
prob += obj

prob.solve(timelimit=2, msg=True)

print("value x0", x0.value())
print("value x1", x1.value())
for clause in clauses:
  print(f"{clause} = {clause.value()}")

Literals

We declear potitive literals using Variable.

# literals
x0 = flopt.Variable("x0", cat="Binary")
x1 = flopt.Variable("x1", cat="Binary")

~x0 represents a non positive literal of x0, e.g. if x0=0 then ~x0=1.

Clauses

or operation of literal is |.

c1 = x0 | x1    # x0 or x1
c2 = x0 | ~x1   # x0 or (not x1)

Objective function

We can create the objective function by arithmetic operation of literals or cluses, or the CustomExpression. For example, \((c_1+2c_2+3c_3+4c_4)\) can be formulated as follows.

clauses = [c1, c2, c3, c4]
weights = [1, 2, 3, 4]
obj = flopt.dot(clauses, weights)

Result

The results of the solver are reflected in the problem and variable objects.

print("value x0", x0.value())
print("value x1", x1.value())
for clause in clauses:
    print(clause)