Solvers by paradigm 29
| Abbrev. | Name | Solvers | Avg. problems |
|---|---|---|---|
| CP | Constraint programmingiVariables range over finite domains and the model states relations between them, often through global constraints such as all-different, element or cumulative. The solver alternates search with propagation, using each constraint to prune the domains of the others. | 11 | 162.7 / 164 |
| |||
| MIP | Mixed integer programmingiEvery constraint is a linear inequality over real and integer variables, and the objective is linear too. Anything that is not linear — a disjunction, an all-different, a product of two variables — must be reformulated, typically by introducing binary variables and big-M bounds. | 7 | 162.1 / 164 |
| |||
| CLP | Constraint logic programmingiConstraint solving embedded in a logic-programming host, so a model is a predicate and its constraints are goals posted over finite-domain variables. The search is a labelling strategy the modeller writes, which makes variable and value ordering part of the model rather than a solver setting. That is what separates it from constraint programming here, and an integration carries this tag instead of the CP one rather than alongside it. | 4 | 162.8 / 164 |
| |||
| MaxSAT | Maximum satisfiabilityiA propositional formula with hard clauses, which must hold, and weighted soft clauses. The solver looks for an assignment that satisfies every hard clause and minimises the total weight of the soft clauses it violates. An objective is written as soft clauses rather than as an expression over variables. | 3 | 164 / 164 |
| |||
| SAT | Boolean satisfiability*iThe model is a propositional formula, usually in conjunctive normal form. There are no integers and no arithmetic: any counting, ordering or numeric bound has to be encoded into Boolean variables and clauses by hand, and the choice of encoding largely decides how well it solves. | 2 | 112 / 112 |
| |||
| SMT | Satisfiability modulo theoriesiA first-order formula interpreted over built-in theories such as linear integer arithmetic. The Boolean structure of SAT is kept, but arithmetic is written directly rather than encoded, so the model reads closer to the problem statement. | 2 | 164 / 164 |
| |||
| ASP | Answer set programmingiThe model is a logic program of rules that a grounder expands over the instance data before a solver searches for its stable models. Choice rules generate candidate answers and integrity constraints reject the ones that break the problem, so how much a rule grounds to is a modelling concern in its own right. | 1 | 163 / 164 |
| |||
| PB | Pseudo-BooleaniConstraints are linear inequalities over Boolean variables with integer coefficients, which keeps SAT's Boolean core while letting counting and numeric bounds be written directly instead of encoded into clauses. An objective is a linear function of the same variables, so optimisation needs no separate machinery. | 1 | 164 / 164 |
| |||
* SAT counts satisfaction problems only.