Questions tagged [constraint-satisfaction]
The constraint-satisfaction tag has no usage guidance.
149
questions
-1
votes
0
answers
16
views
Sequencing swaps with constraints
I have an array of N numbers, and M swaps. Each swap has an index i and amount it subtracts from the ith number, and an index j and amount it adds to the jth number. It can only be applied if the ...
- 99
1
vote
1
answer
47
views
Applications of a SAT Solver Oracle for Determining the Uniqueness of Solutions
I am exploring two kinds of model $π_{π,π,k}$ and $S_{m,n,k}$ within the realm of satisfiability problems (SAT).
Formal construction of $π_{π,π,k}$
To construct the $π_{π,π,k}$ model in ...
- 338
1
vote
0
answers
17
views
"package" compatibility solver with verion ranges
I am looking for how to solve the package compatibility problem. I have found some relevant research and libraries. But some of them are older. I am wondering if there is any more recent research and ...
- 111
1
vote
0
answers
26
views
Resolving distance constraints in 2D
I am currently writing a tool that will be used in an industrial process to place components with physical requirements. It boils down to the following:
I have a set of points (typically, a few ...
- 111
0
votes
1
answer
48
views
Convert ternary constraint into set of binary
I have the following ternary constraint that needs to be converted into a set of binary constraints in order to be used for a constraints solving problem:
...
1
vote
1
answer
324
views
How fast can we make generalized k-SAT?
Suppose a generalized version of k-SAT where the usual clauses
(disjunctions of literals) are generalized to arbitrary Boolean functions of k variables. (For example,
$(x \oplus (y \land z)), ((x \...
- 510
3
votes
2
answers
881
views
How to find a satisfying assignment in polynomial time without the use of randomness?
Assume that we are given a formula in 3-CNF such that at least 1% of
the complete assignments satisfy it.
My question is how to find a satisfying assignment in polynomial time without the use of
...
- 327
1
vote
0
answers
33
views
Understanding Arc Consistency 4 in the context of Wave Function Collapse
Following this blog post about the Arc Consistency algorithms. Namely, the explanation on AC4. Consider the following example:
If I understand AC problems correctly. Then:
We have two known ...
- 111
0
votes
0
answers
14
views
Collaborative Multi Agent Path planning on directional and non-planar graph
I am trying to implement a multi-agent path planning algorithm that works on non-planar graphs and large agents (that is, collisions may at the intersection of two edges and at points where the edges ...
- 51
0
votes
1
answer
40
views
Is minimum interval hitting problem NP-HARD?
Consider this problem:
We want to mark some integer numbers such that we mark the minimum number of the numbers and satisfy some constraints. Each constraint wants that at least $k$ numbers in ...
1
vote
1
answer
89
views
Bipartite matching with constraints on one part
We have a bipartite graph with parts $A$ and $B$, and it is edge weighted. We have some constraints for part $B$. Each constraint is in this format: Between vertices $b_1$ and $b_2$ both from part $B$,...
2
votes
1
answer
64
views
Minimal set of elements needed to satisfy property counts
I have a friend who works in education. Sometimes, they need to create customized "word lists" to help students practice reading. These lists are limited in length, and must contain ...
3
votes
1
answer
113
views
Efficient way to calculate many Dutch auctions?
I have 4,500 ($N$) unique items, and I want to auction each one off to the highest bidder (break ties arbitrarily).
Each item has $T$ binary traits. Since it is too complex for the $B$ bidders to ...
- 151
2
votes
2
answers
178
views
what is the background theory that Z3 uses to prove constraints unsat
The method to get the sat result is kind of straightforward, you can use some search algorithms like heuristic search to get a solution. But how does z3 get the unsat result like x < 2 && x ...
- 21
0
votes
1
answer
101
views
How to solve boolean SAT with equality constraints
Say I have boolean formula in form of a CNF(x1,x2,...) with $x_i$ being boolean variables.
Testing the satisfiability of the CNF is the SAT problem, i.e. determine ...
- 161