# Tag Info

Accepted

### Why don't modern SAT solvers use the notion of a "watched clause", in the same way they use the notion of a "watched literal"?

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

### SAT algorithm for determining if a graph is disjoint

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$ ...
Accepted

### Constraint Satisfaction: maximizing total value with no overlaps

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

### Aren’t most constraining variable and least constraining value the exact opposite?

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

### Efficient algorithm for simple constraint satisfaction problem

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

### How could an SMT solver be implemented as simple as possible?

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

### How do we place $8n$ objects in a grid of size $n \times n$?

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

### Binarization of Constraints

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$. ...
Accepted

### Requiring at least one alldiff constraint to be satisfied converted to SAT

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$ ...
Accepted

### Are finite-domain binary constraint satisfaction problems solvable in polynomial time?

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

### General structure of solutions to 3-SAT circuits

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

### Is every X3SAT instance with no cycles satisfiable?

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

### SAT algorithm for determining if a graph is disjoint

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$ ...
Accepted

### Sum of unique integers to cnf constraint

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

### Linear programming over a finite field

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

### Is the following problem NP-Complete?

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

### Is 2-SAT over Linear Real Arithmetic in P or NP?

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 +...
Accepted

### Theoretical CSPs where (in)equality constraints can be expressed as a single constraint?

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

### Algorithm for solving planar constraint problem ("Pokemon Go monster finding")

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

### What is Least-Constraining-Value?

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

### Contraint with three variables into three binary constraints

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

### How could an SMT solver be implemented as simple as possible?

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