9
votes
Accepted
Aren’t most constraining variable and least constraining value the exact opposite?
Yes, these two heuristics 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 ...
- 39.1k
9
votes
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$ ...
- 279k
7
votes
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 ...
- 22.8k
6
votes
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 ...
D.W.♦
- 166k
6
votes
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 ...
D.W.♦
- 166k
5
votes
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 ...
- 39.1k
5
votes
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$ ...
D.W.♦
- 166k
4
votes
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 ...
- 4,272
4
votes
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$. ...
D.W.♦
- 166k
4
votes
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 ...
- 279k
4
votes
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 ...
- 39.1k
4
votes
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 ...
- 13.9k
4
votes
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 ...
- 279k
4
votes
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 ...
- 5,509
4
votes
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 +...
- 279k
4
votes
what is the background theory that Z3 uses to prove constraints unsat
There are basically two components: the underlying SAT solver procedure (DPLL), and the additional theory-specific procedures.
For the underlying SAT solver: considering your example of ...
- 7,248
3
votes
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 ...
- 23.8k
3
votes
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 ...
- 279k
3
votes
what does it mean to extend an assignment?
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 ...
- 22.8k
3
votes
Accepted
Is this problem that's similar to integer linear programming also an NP-complete problem?
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 +...
D.W.♦
- 166k
3
votes
Selection over combinatorics that satisfies a distribution
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 ...
- 4,662
3
votes
Algorithm to create dense style crossword puzzles
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 ...
- 5,509
3
votes
Automated reasoning with real numbers
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 ...
- 23.8k
3
votes
Accepted
Efficient Algorithm to Find the Closest Integer Representation, in the Form $A\times\frac{N}{D}$ for a Value
Generally speaking, this problem is called diophantine approximation.
However, your inputs are not just real numbers but double-precision floating point (aka double)...
- 3,459
3
votes
Bipartite matching with constraints on one part
The problem is not approximable in polynomial-time within a factor of $n^{1-\varepsilon}$ for any constant $\varepsilon>0$, unless $\mathsf{NP} = \mathsf{ZPP}$.
To see this you can reduce from ...
- 29.6k
2
votes
Modeling tiling problems as SAT problems
One example of a tiling problem that was successfully attacked by reducing it to a SAT instance was rectangular grid coloring. In "Extremely Complex 4-Colored Rectangle-Free Grids:
Solution of Open ...
- 8,149
2
votes
Small world theorem for set constraints
The conjecture is true, and the proof strategy listed there can be made to work.
Let $s = (s_1,\dots,s_n)$ be a satisfying assignment for the variables that makes all of the constraints hold. We'll ...
D.W.♦
- 166k
2
votes
Is there a "well known" example of a constraint satisfaction problem on a 3-element set which is polynomial-time solvable?
If you want a graph, it needs to be bipartite. Hence the path of two edges or any subgraph thereof. (Here I am following the convention that graphs have no loops. As David Richerby points out in a ...
- 2,328
2
votes
Accepted
Mimimum spanning tree with a constraint on number of certain types of edges
Let us take Kruskal's algorithm for an example. Apparently, OP refers to the adjusted version such that when we choose among edges of equal weight, we will pick the ones in $A$ before the ones in $B$ ...
- 39.1k
Only top scored, non community-wiki answers of a minimum length are eligible