The inequality-satisfiability problem

We define a generalized variant of the satisfiability problem (SAT) where each "clause" is an or-list of inequalities in n variables. The inequality satisfiability problem (I-SAT) is to find whether there exists a feasible point in n that satisfies at least one inequality in each "clause". We show that I-SAT is harder than SAT in that I-SAT is NP-complete even when restricted to contain only two inequalities per "clause". We provide here an algorithm for solving an I-SAT on n variables and m "clauses" each containing up to k inequalities, with complexity dominated by O((km)min(n,m)-1 m(kn + log m)). In fact the complexity of the algorithm is polynomial when either the number of variables or the number of "clauses" is fixed. A problem of major interest in manufacturing called the mold casting problem, is shown to be a special case of an I-SAT on two variables and at most 9 inequalities per "clause".

• Type: Journal
• Year: 2008
• Where: ORL
• Authors: Dorit S. Hochbaum, Erick Moreno-Centeno
• Keywords: I-SAT, Inequality Satisfiability Problem, ORL 2008, Satisfiability Problem