Half-SAT problem

The Half-SAT problem can be defined as:

\[\text{HALF-SAT} = \{ \varphi \mid \varphi \text{ is a formula which is satisfied by half of all assignments }\}\]

Or, in other words, considering a CNF formula with \(2n\) variables, an there’s a satisfying assignment in which \(n\) variables are True and \(n\) variables are False. The Half-SAT problem is known to be NP-Hard, so it cannot be solved in polynomial time. In these situations the Particle Swarm Algorithm can sometimes reach optimal results in an feasible amount of time

Out:

Iteration 0:
   global_best: 1.000   iteration_best: 1.000   hamming: 0.950

Iteration completed
==========================
Exit code 2: Algorithm has reached the value threshold of 1
Elapsed time 0.012
0 iterations
Best selection: [3, 5, 7, 11, 13, 16, 18, 19, 21, 23, 24, 25, 26, 27, 29]
Best evaluation: 1.0

import random
from psopt import Combination


def generate_cnf(n_vars, clauses, k=3, seed=None):
    """
    This function generates a random CNF formula for the Half-SAT problem

    Args:
        n_vars (int): the number of variables in the formula

        clauses (int): the number of clauses that compose the formula

        k (int, optional): the number of variables in each clause. Defaults to 3

        seed (int, optional): Seed the function generator

    Returns:
        cnf (callable): a function in CNF for the Half-SAT problem
    """
    # seed value for testing purposes
    random.seed(seed)
    # start expression
    cnf = str()
    # iterate clauses
    for _ in range(clauses):
        clause = str()
        # get variables
        variables = random.sample(list(range(n_vars)), n_vars)[:k]
        # build clause
        clause += random.choice(["", "not "]) + "x[{}]".format(variables.pop(0))
        while len(variables) > 0:
            clause += " or {}x[{}]".format(
                random.choice(["", "not "]), variables.pop(0)
            )
        cnf += "({}) and ".format(clause)
    # quick-fix for pattern that does not affect the result
    cnf += str(1)
    return lambda x: eval(cnf), cnf


def main():
    # define objective function: SAT in CNF
    n_var = 30
    fn, desc = generate_cnf(n_var, 20, seed=0)

    def obj_func(x):
        return fn([1 if i in x else 0 for i in range(n_var)])

    # instantiate the optimizer
    opt = Combination(obj_func, list(range(n_var)), metrics="hamming")

    # define a threshold of acceptance
    threshold = 1

    # Uncomment line below to display the objective function
    # print("Objective function: \n{}".format(desc)

    # maximize HALF-SAT
    # (half of the number of variables are one and the rest is zero)
    opt.maximize(selection_size=n_var // 2, verbose=1, threshold=threshold, seed=0)


if __name__ == "__main__":
    main()