6
$\begingroup$

I have a linear programming problem $LP$ where all the variables $x_{i}$ take value in $\left[0, 1\right]$ (that is $0\leq x_{i} \leq 1$). All the constraints are as follow: $a_{1}+a_{2}+a_{3}=1$ that is each constraint is the sum of three distinct elements, for each elememt $a_{j}$ with $j\in \left\{1; 2; 3\right\}$ we have $a_{j}=x_{i}$ or $a_{j}=1-x_{i}$ and each sum is equal to $1$. It is not possible that the same variable $x_{i}$ appears two times in the same sum.

If for each variable $x_{i}$ we have that $LP$ is feasible whether we set $x_{i}=0$ or $x_{i}=1$, can we say that exists an integer solution of $LP$, that is a solution where each variable takes value in $\left\{0; 1\right\}$?

I give an example to make clearer my question.
Given:
$x_{1}+x_{2}+x_{3}=1$
$x_{4}+(1-x_{5})+x_{6}=1$
$(1-x_{7})+x_{8}+x_{9}=1$
$(1-x_{1})+(1-x_{5})+(1-x_{7})=1$
$0\leq x_{i} \leq 1$ $\forall i$

Foreach variable $x_{i}$ of the problem, one by one, we have that the problem is feasible whether we set $x_{i}=0$ or $x_{i}=1$.
The problem has at least an integer solution: $x_{1}=1$, $x_{2}=0$, $x_{3}=0$, $x_{4}=1$, $x_{5}=1$, $x_{6}=0$, $x_{7}=0$, $x_{8}=0$, $x_{9}=0$.

The question is: in general, for a problem where the constraints are the sums of three variables or their complement to $1$, the sums are equal to $1$ and $0\leq x_{i} \leq 1$ $\forall i$ (like in the given example), is it true that if the given problem is feasible whether we set, one by one, $x_{i}=0$ or $x_{i}=1$ foreach variable $x_{i}$ of the problem, then there is at least an integer solution of the given problem?

$\endgroup$
7
  • $\begingroup$ I find your problem description to be confusing. Are you saying that the constraints are $0 \le x_i \le 1, \sum_{i=1}^3 x_i=1$, and that these are all the constraints? Then you want to know whether the same problem, but with $x_i$ constrained to be zero or one, has the same optimal objective value as allowing $x_i$ to be continuous? $\endgroup$ Mar 17 at 18:05
  • $\begingroup$ The constraints $0\leq x_{i} \leq 1$ are right, but about the sums I have constraints like $x_{i}+x_{j}+(1-x_k)=1$, $(1-x_{l})+x_{j}+(1-x_h)=1$, $(1-x_{i})+x_{g}+(1-x_l)=1$ and so on, that is each constraint is the sum of three elements, each element is a variables of the problem ($x_{i}$) or its complement to $1$ ($1-x_{i}$) and each sum is equal to $1$. $\endgroup$ Mar 17 at 20:37
  • $\begingroup$ If the original problem has a solution for which the variables are not all either 0 or 1, then if a constraint that all variables are 0 or 1 is added, the resulting problem is not necessarily feasible, and therefore the original optimal objective value can not be achieved. But this doesn't seem to be what you are asking. Or does it answer, n the negative, what you really meant to ask? $\endgroup$ Mar 17 at 21:40
  • $\begingroup$ I have added an example to my question that should make clear what I mean. $\endgroup$ Mar 18 at 2:46
  • 1
    $\begingroup$ Interesting question. If I understand correctly, the requirement is that for any one variable in the problem, constraining that variable either to 0 or to 1 (with all others constrained between 0 and 1, but not necessarily integer) leaves the problem feasible. I would have expected that this would not guarantee that a fully binary-constrained version of the problem is feasible, but I haven't yet got a counterexample. $\endgroup$ Mar 18 at 5:32
3
+25
$\begingroup$

If I am not mistaken the answer is NO unless $P=NP$. We can reduce Exactly-1 3-satisfiability to your problem. For a proof of 1-IN-3SAT is NP-complete see NP-Completeness of 3SAT, 1-IN-3SAT and MAX 2SAT.

Given an instance $I$ of the Exactly-1 3-satisfiability problem. For each variable $x_i$ check whether there is a solution setting it to $1$ and $0$. This can be done solving $2n$ LPs. Then there are three cases:

  1. All variables have a solution with $1$ and $0$. Then we are in the case you described and we know there is an integer solution.
  2. There is a variable with no solution for both cases ($1$ and $0$). Then we know there is no solution for the entire problem.
  3. None of the above is the case and there are variables satisfying exactly one of the two cases. Then we can fix these variables to the cases that do work and reduce the problem size. During this reduction we have to do some extra work described in the following.

In step three we might end up getting constraints of the form: $$ \begin{align} a_1 &= \begin{cases} 0 \\ 1\end{cases}\\ a_1+a_2 &= 0 \\ a_1+a_2 &= 1. \end{align} $$ In the first case we can simply fix the variable encoded in $a_1$ and continue cleaning up. The same holds for the second case, where we get $a_1=a_2=0$.

For the third case we can replace the variable in $a_2$ by the variable in $a_1$ such that the constraint is always fulfilled ($a_2 = 1-a_1$). By this it might happen that we end up getting constraint containing one $x_i$ multiple times. This is also not a problem, as this either fixes $x_i$ to be always $1$ (in cases we have $2x_i$), always $0$ (in cases we have $2(1-x_i)$) or adding a constant to the constraint (in cases $1-x_i+x_i$). In this case $x_i$ can be removed from the constraint and either the constraint disappears entirely or we end up with something like $a_1 = \begin{cases} 0 \\ 1\end{cases}$, which we already solved.

If during this reduction we find the problem to be infeasible we know it is infeasible. Otherwise we can start over on a smaller problem.

After at most $n$ iterations all variables were replaced or we ended up with case 1. or 2., thus the algorithm terminates in polynomial time.

I hope this helps and in case I made any mistakes please point them out. ;)

$\endgroup$
8
  • $\begingroup$ Do i understand it correctly that assuming your reply is correct, however there is no instance of 4 variables for which OPs question isn't true that that would mean that P=NP? Since OPs problem space is enumerable (has less or equal than 2^(2^3*(n over 3)) and for n=4 variables we are looking at 2^32 MILP problems without symmetry arguments) searching that space would either find a small counter example to OPs question or tells us P=NP for small n. $\endgroup$ Aug 28 at 12:17
  • 1
    $\begingroup$ There is no such thing as $P=NP$ for small $n$. Either the OPs statement holds for all $n$, that's infinitely many and you can't try all of them, or you won't find $P=NP$. $\endgroup$
    – SimonT
    Aug 28 at 14:47
  • $\begingroup$ If you can show $P = NP$ for a small $n$ and build an induction on that you can show it for all $n$. Or if ti works for all at some $n$ but no longer for all at some $m+1$ there might be an insight into improving the algorithm or why $P \neq NP$. Anyway if you don't consider the notion for $P = NP$ for some class of size limited problems to be worth i will not investigate or attempt to find a traceable counter example. $\endgroup$ Aug 28 at 20:38
  • $\begingroup$ @SimonT Why, when all variables have a solution with $1$ and $0$, is there an integer solution (case 1.)? $\endgroup$ Aug 28 at 20:57
  • $\begingroup$ @Mario Giambarioli If I understood correctly that was assumption you had in your question $\endgroup$
    – SimonT
    Aug 28 at 21:05
1
$\begingroup$

The question can be understand as determining the truth value of $$(\forall \text{assignments}: \text{relaxation feasible} )\implies \text{problem has integer solution}.$$

However since setting up many LP problems is more expensive then solving a small MILP (or even cheaper 1-in-3 SAT). I instead try to show the opposite: $$(\forall \text{assignments}: \text{relaxation feasible} )\land \neg(\text{problem has integer solution)}.$$

A not quiet naive approach that works for 4 variables

I tried to find an counter example but wasn't able to put in the engineering effort to remove all the symmetries so my approach only scales to 4 varibles.

I attempted to do that for all 4 variable formulas with the following (hacky and ugly) Julia code.

using JuMP
using Gurobi

coll = []

function build_constraint(model, vars, constraint)
  rhs = 1
  signs = similar(constraint)
  for i in eachindex(constraint)
     if sign(constraint[i]) == -1
       signs[i] = -1
       rhs -= 1
     else
       signs[i] = 1
    end
  end
  @constraint(model, sum(signs[i]*vars[abs(constraint[i])] for i in eachindex(constraint) ) == rhs)
end


function flip_signs(head,tail,func)
  if isempty(head)
    func(tail)
  else
    hd = head[1]
    for i in Iterators.product(-1:2:1,-1:2:1,-1:2:1)
       c =  copy(tail)
       flip_signs(head[2:end], push!(c, i .* hd), func)
    end
  end
end
      
      
function build_model(constraints)
  m = Model(Gurobi.Optimizer)
  @variable(m,x[1:4],Bin)
  for c in constraints
    build_constraint(m, x, c)
  end
  set_silent(m)
  optimize!(m)
  if termination_status(m) != MOI.OPTIMAL
    println("Interesting: ",constraints)
    push!(coll, constraints)
  end
end

flip_signs([[1,2,3]], [], build_model)
flip_signs([[1,2,3],[1,2,4]], [], build_model)
flip_signs([[1,2,3],[1,2,4],[2,3,4]], [], build_model)
flip_signs([[1,2,3],[1,2,4],[2,3,4],[1,3,4]], [], build_model)

counter = []

function build_linear_models(collection)
  for constr in collection
    m = Model()
    @variable(m,0<=x[1:4]<=1)
    for c in constr
      build_constraint(m, x, c)
    end
    isalwaysfeasible = true
    for i in 1:4
      for v in 0:1
        m2 = copy(m)
        set_silent(m2)
        set_optimizer(m2, Gurobi.Optimizer)
        @constraint(m2, variable_by_name(m2,"x[$(1)]") == v)
        optimize!(m2)
        isalwaysfeasible = isalwaysfeasible && (termination_status(m) == MOI.OPTIMAL)
      end
    end
    if isalwaysfeasible
      push!(counter,constr)
      println("Counterexample: ", constr)
    end
  end
end
        
build_linear_models(coll)        
        
if isempty(counter)
  println("nothing found")
end     

I first collect all instances Gurobi couldn't solve successfully and then check whether any of these passed the relaxation test. I found no counter examples with 4 variables. I did that by checking the 4 equivalence classes of hypergraphs made solely out of 3-hyperedges that cover a 4 element fully connected graph. There are 4 of them and then try every single sign flipped version of 5. This however scales really badly for 5 variables. As the formula containing all distinct 3 literal clauses of 5 variable are of count $2^{3\binom{5}{3}} = 2^{30}$ of which a larger fraction are redundant. (Think 1 in sum over some factorials is not a duplicate, did not make a more precise analysis but 1 in 10! is an overestimate of the degree of duplication.

How would i go about it if it was my job

This problem quickly becomes intractable as naive approaches would already fail at 4 variables and my slightly advanced approach of generating the which variables are inside a clause independent of the conversion into literals fails for 5 variables. (By failing i mean takes to long and next step will be much, much worse (I think i could make a good case for super-exponentially worse))

The biggest priority is write a system that generates one example for every equivalence class of non-redundant 3 sat formulas. Two formulas are in the same equivalence class if there exist an one-to-one and onto mapping from the variables and their negatives into the variables and their negatives such as the formula matches all solutions can be translated into solutions of the other formula using that mapping.

The approach is to construct from the empty formula (or deconstruct from the full formula) a 3-hypger graph where each 3-edge doesn't violate the variable occurs twice rule.

You see nodes for the literals $1$ thtough $4$ and their negation. A 3 hyperedge is only valid if each node it connects is directly to connected to every other node in the 3-hyperedge in the graph above. Notice the absence of connection between literal and their negation to enforce your constraint.

To prevent the creation of redundant formulas it essential (and probably sufficient) to track symmetric literals/nodes 1 in the 3-hypergraph and when expanding the search tree on that node don't expand it in a way which would add two child nodes which have a new 3-edge that is identical given the node symmetries in the parent. Another thing to be aware is that the search tree is actually a Directed Acyclic graph, as there are multiple ways of adding hyperedges to end up with same hypergraph. So a checking for 3-hypergraph equivalence needs to be performed between every hypergraph at each depth. There are some heuristics that can allow you to bail out early when comparing and i haven't explored but find it likely that the DAG structure might also poses constraint which nodes can bring forth similar equivalent children.

Also note that adding an edge can include up to 2 literals which weren't in the parent and their negation wasn't either, however not 3 literals which weren't in the parent as you are only interested in growing connected 3-hypergraphs, as non connected ones are independent sub problems with fewer literals you would have searched when you did a run with that many variables. It is possible to add 3 new literals though if one of the has a negation in the parent.

For $n$ variables the will be graphs with length from 0 to $\binom{n}{3}$ this search DAG however there is an symmetry in the search DAG i hinted at the beginning, namely a $m$ 3-edge hypergraph has $\binom{n}{3} - m$ 3-edge hypergraph as negation.

An algorithm that satisfies these notes should be able generate only one and one member from all equivalence classes of that many variables. However a formal treatment might discover i missed something.

The next most important thing is to speed up the batch solving of the very, very similar LP problems that arise. It is possible GPU acceleration is beneficial here.

The last step at scale is to modify an existing fast starting SAT solver into an 1-in-3 SAT solver, as that the 1-in-3 SAT problems can be solved a lot faster that way than an SAT encoding. It would be furthermore advisable to remove presolving. If this becomes a larger bottleneck it might be worth to look into SAT solvers for random formulas as they have special techniques that could work well when ported over to 1-in-3 SAT.

A last thing into keep in mind is that the LP check and the 1-in-3 SAT call can be easily distributed even on something with as weak coupling as BOINC. If you have more workers than you can satisfy with one computer producing the equivalence class representatives you can have a second computer works on generating problems a different number of variables. The reason why i want to discourage distributing this part is that you need and all to all nodes in the search DAG communication and 3-hypergraph equivalence checks across these links (this would be possible with MPI in an HPC environment but i imagine the pain not being worth it until you start to run out of memory on as a big a server as you can afford having many of). The equivalence class generation happens more efficiently on a single node and there are no two points you can start searching independently (expect empty and full but you can generate the other by inverting the other anyway) without risking duplicate clauses or having to check for equivalence later. One equivalence when expanded leads all children also being explored redundantly.

Solving this problem in scalable way will require a non-trivial new algorithm, modifying exiting libraries, new research into batch LP solving. If it doesn't find an counter example it wouldn't completely wasted as it will probably yield new insights into SAT solvers as the study of the equivalence classes might reveal new patterns.

This post should give you a good battle plan how two researchers could setup this in a few months. I can make no estimate on how much compute will be needed, as we don't know how the number of equivalence classes of 3-SAT instances (without repeated variables) scales with the number of variables.

Another approach to falsification: Encode hard SAT formulas into 1-in-3 SAT and check your prediction vs the know result agreed upon multiple solvers.

1 Generalize this notion of graph symmetry to 3-hypergraphs

$\endgroup$

Your Answer

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

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