11

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear ...


9

Given a graph $G = (V,E)$, here is a SAT instance which is satisfiable iff the graph is not connected. Pick an arbitrary vertex $v_0 \in V$, and add the following clauses, over the variables $x_v$ for $v \in V$: $x_{v_0}$. For every $(u,v) \in E$, $\lnot x_u \lor x_v$ and $\lnot x_v \lor x_u$. $\bigvee_{v \neq v_0} \lnot x_v$. Here is a SAT instance which ...


7

You are looking for a maximum weight independent set in an interval graph, which can be solved in linear time (by a deterministic algorithm). By the way, the same is true also for a superclass of interval graphs, namely chordal graphs. One such algorithm is based on dynamic programming, you can see e.g., [1] for details and discussion. [1] Hsiao, Ju Yuan, ...


7

Yes, these two heuristics does sound like inconsistent. Most Constrained Variable (MCV) (also called MRV for Minimum Remaining Values) tries to reduce the size of the next branch to search while Least Constraining Values tries to enlarge the size of the next branch to branch. However, if you take a close a look, they both serve the same goal, which is, given ...


6

There is unlikely to be any efficient algorithm. Your first class of constraints are monotone exactly-1 CNF clauses. Your second class of constraints are monotone CNF clauses. The monotone part indicates that negated literals aren't allowed (you can't have $x_1 - x_3 = 1$ or $x_1 - x_4 \ge 1$). Thus, in the special case where you have only type-2 ...


6

What happens next is that we invoke a SMT solver to try to check whether the formula $$x+y < 20 \quad \land \quad x > 10 \quad \land \quad y > 10$$ is satisfiable. The solver tries to find values for $x,y$ that make this formula true. If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to ...


5

Given a set of objects in a cell grid, if no 4-set of it forms a rectangle with sides parallel to the sides of the grid, we will call those objects rectangle-free. The more general problem is to determine sequence A072567, whose $n$-th term $M_n$ is the size of maximal set of rectangle-free cells in an $n \times n$ cell grid. Its first 13 entries are $$1, ...


4

Introduce a new variable $Q$, whose domain is $\{0000,0001,0010,\dots,1111\}$. It represents the value of $C1,C2,C3,P$. For instance, if $Q=0001$, that means that $C1=0$, $C2=0$, $C3=1$, $P=0$. Then, you add a constraint that the first bit of $Q$ is equal to $C1$ (that's a binary constraint), a constraint that the second bit of $Q$ is equal to $C2$ (...


4

If you want to model an alldiff() constraint in SAT, there are several options. Here are two different options you can try: One way is to expand $\text{alldiff}(x_1,\dots,x_n)$ into $n(n-1)/2$ inequality constraints: $(x_1 \ne x_2) \land (x_1 \ne x_3) \land \cdots$. Now you can express each inequality constraint $x_i \ne x_j$ on $b$-bit values in turn as ...


4

I don't know, but if you manage, make sure to let us know. The reduction seems easy indeed, with $d$ mapping to the number of colors and each constraint to an edge. However, a polynomial-time algorithm for any $\mathcal{NP}$-complete problem exists if and only if $\mathcal{P} =\mathcal{NP}$; doing what you ask would imply $\mathcal{P} \neq \mathcal{NP}$.


4

The theory you are after is universal algebra. See the excellent expository article of Hubie Chen, A rendezvous of logic, complexity, and algebra, which contains a streamlined proof of Schaefer’s dichotomy theorem, which was recently extended to arbitrary alphabets. 3SAT has no polymorphisms. NAE-3SAT has only negation as a polymorphism. All other classes ...


4

The graph below is a positive answer without words. Here is the detailed proof. Definitions Let $X$ be an instance of X3SAT. $X$ is linear if any two clause shares at most one variable. $X$ is monotone if all literals in all clauses are positive. A walk in $X$ is a sequence of clauses where each clause is not disjoint with the clause following it. The ...


4

Yuval describes a boolean CNF formula that is satisfiable iff the graph is not connected, using $|V|$ variables; and a boolean CNF formula that is satisfiable iff the graph is connected, using $|V|^2$ variables. I describe here a boolean CNF formula that is satisfiable iff the graph is connected, using $O(|V| \lg |V| + |E|)$ variables. If $|V|$ is large ...


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 \...


4

Your problem, solving a system of linear equations, can be solved using an ancient algorithm, Gaussian elimination, which works over all fields. Note that linear programming is more general, allowing also inequalities. It is not entirely clear, however, how the order should be defined over a finite field.


4

No. This problem is equivalent to XOR-3SAT, in which we interpret each clause as $x \oplus y \oplus z$, where $\oplus$ is the XOR operator, and ask whether it's possible to find values for all variables so that each clause is true. XOR-SAT can be solved in polynomial time using Gaussian elimination, with all arithmetic done modulo 2 (i.e., in the finite ...


4

You can express the fact that a variable $x_i$ is Boolean as follows: $$ (0 \leq x_i \leq 1) \land ((x_i \leq 0) \lor (x_i \geq 1)). $$ You can express the condition $x_i \lor x_j \lor x_k$ as $$ x_i + x_j + x_k \geq 1. $$ If some of the variables are negated, you can also accommodate that, by replacing $x_i$ with $1-x_i$. In total, we can express SAT as a ...


3

In complexity theory, CSPs are usually specified as a set of allowed predicates. If the (finite) domain is $D$, a predicate of arity $d$ is an arbitrary subset of $D^d$ of allowed values. In particular, equality (or inequality) is a predicate of arity 2. This is the point of view taken in Schaefer's dichotomy theorem as well as the more recent universal ...


3

I think you could use a "spatial join". I haven't played the game, but I assume $d_{max}$ is rather small, i.e. there are in the order of 10 or so $n$ and $m$ in the neighborhood of each $m$. I further assume that $N$ and $M$ are large, say 1,000,000 or more. Put all $m$ as 2D points in a spatial index For each $m_1$ in the index, perform a spatial range ...


3

see this link: https://people.cs.pitt.edu/~wiebe/courses/CS2710/lectures/constraintSat.example.txt It first picks variable "O" and then tests "O" with all of it's legal values "i" to see the number of reductions on "O"'s neighbors "N". It adds all of them. and picks an "i" that causes less reductions: sums = {0:0,1:0,2:0,3:0,4:0,5:0,6:0,7:0,8:0,9:0} ...


3

Good question. Your instinctive reaction is quite valid: if you stick with the variables $A,B,C$, there is no way to introduce some set of binary constraints that will be equivalent to $A+B=C$ (where each constraint is only allowed to mention two of $A,B,C$). The trick is to introduce new variables, or change the set of variables. If you do that, it can ...


3

You may not need a general SMT solver. In this case, you have a bunch of inequalities conjoined together, which you can solve as a linear program. A simpler alternative to an SMT solver is to implement the theory as an add-on to a logic program. Most decent Prolog implementations, for example, have a CLP(R) or CLP(Q) library which can solve equality and ...


3

It means that you have a partial solution, and you extend that partial solution by assigning at least one more variable to some value, thus producing either a new partial solution or a solution where every variable is assigned a value. Put differently, if $x$ extends an assignment $a$, it holds that $x$ does precisely the same assignments as $a$ and assigns ...


3

Your problem is solvable in polynomial time. Your problem is equivalent to ILP with difference constraints, i.e., every linear inequality has the form $x_j - x_i \ge c_{i,j}$. (Why? Set $x_i = v_1 + \dots + v_i$; then $v_{i+1} + \dots + v_j = x_j - x_i$.) Such a system of inequalities can be solved with shortest-path algorithms. In particular, if we ...


3

Consider the following special case where for each element $i$ the table contains the constraint $\#i \geq (1/l) \cdot l$. This means we need to select the sets in such a way that each element appears at least once. This problem is called the set covering problem, where you have to output whether there is a subset of $l$ sets in the input that covers all the ...


3

There may simply be no solution to some of these problem instances. And the fact that the problem is NP-hard means that you cannot expect to find any efficient algorithm to find solutions for large instances, even if they do exist. That said, I suggest the following relaxation: Idea: Map down to a smaller alphabet Choose some $k < 26$, and map each of ...


3

In your case, the simplest solution may be to use SAT. Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in ...


3

Generally speaking, this problem is called diophantine approximation. However, your inputs are not just real numbers but double-precision floating point (aka double) numbers, which are in fact rational. Any double number has the form: $$ (-1)^{sign} ( 1 . b_{51} b_{50} ... b_{0}) \times 2^{e - 1023} $$ where $b$ encodes the mantissa (52 bits) and $e'=e-1023$ ...


2

The variable $T$ is not a timer but the temperature. It starts very high, making it more likely that transitions are taken, and then slowly cools. It's called annealing due to the metallurgical technique of the same name. Simulated annealing handles one problematic aspect of the hill climbing algorithm, namely that it can get stuck at a local optimum which ...


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