9

There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from ...


5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


5

There are no competitions targeting general integer programming or mixed integer programming, but there are (or were) benchmarks, such as the MIPLIB (linear) and the MINLPLIB (nonlinear). There are competitions for subsets (PB, SAT, max-SAT) and for constraint programming, as you and other answers pointed out. You can find many competitions (DIMACS ...


5

There are competitions for constraint satisfaction solvers. Some problems there can be readily translated to IP solvers as well. See e.g., MiniZinc challenge which has taken place yearly since 2008 or the XCSP competition.


4

Here's a strategy for solving Kakuro with a SAT solver. Make a nine variables for each cell, each variable indicating whether that cell contains $1$, $2$, etc. Add a exactly-one-out-nine constraint for the variables of each cell. You can do this naively in 37 clauses by adding a clause that at least one of the nine must be true ($x_1 \vee x_2 \vee \dots \...


3

Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones. You could explore to see whether this offers a speedup in your situation. There are no guarantees, and the only way to tell is to try it.


3

There was a Pseudo-Boolean solver competition from 2005-2012, but (as far as I can tell) nothing since then. Integer Linear Programming is a subset of Pseudo-Boolean programming. See the 2012 competition page for results and links to other competition results.


3

All the literals in a conflict clause are set false by definition, else there would be no conflict. So if the clause $\overline{b_1}\lor\overline{b_2}$ existed, one of those false literals would have caused that clause to go unit before we reached the current level, which in turn would have forced one of the $\overline{b_1}$ or $\overline{b_2}$ literals ...


3

With SAT, it can be challenging to predict what will be feasible and what won't. It's worth a try. I would suggest that, instead of MinSAT, you first try using binary search on $n=|\mathcal{S}|$, the number of sets you need. You can use an at-most-$n$-out-of-12376 constraint on your $X_S$ variables. There are several techniques for encoding that in SAT, ...


3

Optimization with SAT is usually referred as MaxSAT instead of Min SAT. In particular, I suggest looking for solvers for "weighted partial MaxSAT", for example MaxHS and RC2. The problem size you have is fairly small in the context of modern MaxSAT-solvers, so yes it is worth trying. There are no guarantees that the solver will work efficiently, and it is ...


2

Here is an $n^{O(k)}$-time SAT algorithm: try all (at most $n^k$) ways how to select one literal from each clause, and accept whenever the selection is such that it does not include any contradictory pair (i.e., a literal and its negation). So, if $k$ is substantially smaller than $n$, you get a subexponential algorithm, and you should not be able to prove ...


2

do we know for which $n_0$ these assumptions "kick in" in the case of $3-SAT$? Can we generate, or at least be confident of the existence of a relatively small formula ($< 200$), such that every algorithm requires $\sim2^{200}$ operations? $3-SAT$ is known to be solvable in time $O(1.321^n)$. Therefore, there is no instance that would force a $\Omega(2^...


1

There is no heuristic that is "universal" in practice. Which heuristic works best in practice often depends on the specific problem you're dealing with. There's no one "silver bullet" heuristic that works great on every optimization problem.


1

Your problem is NP-complete, even when the range of the $x_i$ has size 3. Consider a 3SAT instance with $m$ clauses. We will construct an instance of your problem with $m$ variables $x_1,\ldots,x_m$. The value of $x_i$ will denote the literal satisfied in the $i$th clause. Correspondingly, if the $a$th literal in the $i$th clause is the negation of the $b$...


Only top voted, non community-wiki answers of a minimum length are eligible