New answers tagged


The standard way to create soft constraints in MaxSAT is to use label variables: For each $AMO_j$ constraint, create a new variable $l_j$. Then create an unit clause $(\lnot l_j)$ with weight $1$ and add the literal $l_j$ to every clause of the standard $AMO_j$ encoding that contains only hard (infinite weight) clauses. Now the label variable $l_j$ acts ...


There are problems for which there is no reduction to SAT that is of P complexity. Those problems may or may not be solved by computations that can be performed in O(2^n) or less time and space. SAT is always worst case O(2^n) or less by definition. SAT has a P complexity solution. See


The correct answer is that the determining if a solution exists and determining a solution are computationally distinct. Not all methods for determining if a solution exists can produce a solution. There exists a solution to the Hamiltonian Path problem that can determine if a path exists but cannot produce any such path. That said the question is made moot ...


The decision versions of both MaxSAT and integer programming are in fact NP-complete, so there is polynomial reduction from integer programming to MaxSAT. In the context of solvers, modern MaxSAT solvers support "weighted partial MaxSAT"-encodings (weighted clauses with possibly infinite weights), so you can add any SAT encoded hard constraints by encoding ...

Top 50 recent answers are included