Given a set of constraints, I want to check whether the constraints are feasible. What I am trying now, is to feed the constraints to a solver and check if the solver returns infeasible. I am using both CSP solvers and optimzation (such as MILP) solvers (in the latter case, I set a dummy objective function, e.g., maximize a constant).

This works, so I can check if a given set of constraints is feasible. However, now I am looking for a more general problem: How many set of constraints are infeasible. One way to do this is to generate all sets of constraints separately, and then feed each of them individually to the solver. Alternately, I can ask the solver to enumerate all solutions, then check which ones do not appear in. Both becomes impractical in my case, as the search space is too big to exhaustively enumerate.

The question is, is there any practical way to find the sets of constraints which are infeasible by using standard CSP/optimization solvers?

Since the question is too broad, let me give a more specific example. Assume, we have 4 binary variables, $x_0$, $x_{1}$ and $y_0$, $y_{3}$. There are certain constraints (say, $x_0+x_1 = 1$, $x_0+y_0=1$, $y_1=1$) which are satisfied only for $(x_0, x_1, y_0, y_1) = (0, 1, 1, 1), (1,0,0,1)$; hence the rest 14 quadruples are infeasible (which I am interested in). In the first method, I am generating all 16 constraints and checking which ones are infeasible. In the second, I am asking the solver for all solutions and taking those 14's which are not present in the solution. In my case, the number of variables are too large (say, $x_0, \ldots, x_{127}$ and $y_0, \ldots, y_{127}$), so no method will work in practice.

Modern CSP solvers can check for feasibility for thousands of variables. What I am looking for is kind of the opposite direction: Can it look for non-feasibility?

  • $\begingroup$ You seem to be interested in counting the number of solutions, i.e. #SAT or #CSP. There should be off-the-shelf tools for these. $\endgroup$ – Yuval Filmus Jan 6 '19 at 8:20
  • $\begingroup$ Could you list „all 16 constraints“ in your example? $\endgroup$ – Marcus Ritt Jun 12 '19 at 20:39

If your system of constraints is expressed as a SAT instance, then this is known as the MAX-SAT problem. MAX-SAT is harder than SAT, but there are standard algorithms. The case of other discrete constraints can be reduced to Weighted MAX-SAT.


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.