Kyle Jones
  • Member for 9 years, 10 months
  • Last seen this week
  • Seattle, WA
Recipe book for SAT encodings?
Accepted answer
10 votes

I read a survey paper a few years ago that seems relevant, "Successful SAT Encoding Techniques" by Magnus Björk. Abstract: This article identifies good practices for SAT encodings by ...

View answer
Is finding a solution of a satisfiability problem harder than deciding satisfiability?
Accepted answer
19 votes

As mentioned in a comment, any method of determining satisfiability of a Boolean formula can be easily converted into a method for finding the satisfying variable assignment. This is because Boolean ...

View answer
Neural Network Weights per input nodes
Accepted answer
1 votes

Yes, each input value is weighted before being fed into the nodes in the next layer. Each input/output pair of "neurons" has its own weight and it is these weights that are adjusted by the neural ...

View answer
Detection of redundant boolean constraints
3 votes

The simplification you're describing is called subsumption. It's a standard technique and some SAT solvers (e.g. minisat) will apply it along with other simplification techniques as a preprocessing ...

View answer
Reduce Set problem to SAT
Accepted answer
4 votes

The final constraint you need to encode is that $k$ or fewer variables in the set ${x_1, x_2, ..., x_n}$ is set true. There is a good reference question that outlines several methods for encoding a 1-...

View answer
Example for an unsatisfiable formula that can be made satisfiable by reordering quantifiers
1 votes

This $\qquad \forall x \exists z \space (x = z)$ is a true QBF. Whatever Boolean value $x$ is set to, $z$ can be set to match. Translated to quantified CNF: $\qquad \forall x \exists z \space (x \...

View answer
Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?
4 votes

Yes. The quantifiers can be ignored for the sake of the test since a quantified Horn formula is syntactically identical to an unquantified one except for the quantifiers. That is, a quantified Horn ...

View answer
Is the "subset product" problem NP-complete?
Accepted answer
13 votes

A comment mentions a reduction from X3C to SUBSET PRODUCT attributed to Yao. Given the target of the reduction it wasn't hard to guess what the reduction was likely to have been. Definitions: EXACT ...

View answer
NP-complete problems not "obviously" in NP
Accepted answer
19 votes

There are at least four such $NP$-complete problems listed in the appendix of Garey and Johnson's COMPUTERS AND INTRACTABILITY: A Guide to the Theory of NP-Completeness. [AN6] NON-DIVISIBILITY OF A ...

View answer
Concept used in the proof
5 votes

An unquantified CNF formula consisting of clauses containing a single positive literal plus any number of negated literals is always satisfiable. To produce a satisfying assignment, you simply set ...

View answer
What is wrong with this seeming contradiction with a paper about AND-compression of SAT?
Accepted answer
12 votes

The confusion arises from a misunderstanding of what being polynomial in the size of the largest instance means. It does not mean that polynomial growth of the compressor's output is allowed as the ...

View answer
Solving SAT using tableau calculus
Accepted answer
7 votes

It can be, but the solution process is equivalent to converting a CNF formula to DNF, which is NP-hard. You will at worst end up exploring an exponential number of disjunction branches.

View answer
Quantifier String Placement
1 votes

If, as I suspect, you are still trying to convert quantified 3-CNF formulas into quantified mixed Horn formulas, the answer is that quantifiers for the newly added bridge variables can be placed ...

View answer
Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality
Accepted answer
1 votes

Use a SAT solver that also allows you to express pseudo-Boolean constraints. Encoding the verification of the existence of the tiling of an NxN grid as a CNF formula is straightforward. Each grid ...

View answer
Why does appending permutations of servers at the end of hash table avoid bottlenecks?
Accepted answer
5 votes

Adding permutations isn't about preventing slow servers from becoming bottlenecks, rather it's about dispersing a convoy once one forms behind a slow server. Because of the way tract locations are ...

View answer
Can one reduce a problem of unknown complexity to a hard problem to show hardness?
6 votes

The proof is not correct. As you've indicated the reduction needs to go in the other direction, i.e. integer programming must be reduced to their problem, not the other way around.

View answer
Resolution and what it means to derive the empty set
2 votes

You seem to be trying to describe and use the resolution proof system. Two points: The resolution rule is only applied to two clauses at a time. The resulting clause, the resolvent, can be added to ...

View answer
Are there more easy SAT Problems?
7 votes

(1) is hard to answer unless you clarify what you mean by "versions of SAT problem." If we limit ourselves to the classes listed in Schaefer's "The Complexity of Satisfiability Problems", the only ...

View answer
Is the DPLL algorithm complexity in terms of # of clauses or # of variables?
Accepted answer
4 votes

In the papers I've read the time complexity of DPLL is expressed in terms of the number of variables in the CNF formula. Using the number of clauses is inappropriate in general because it is known ...

View answer
Encoding 1-out-of-n constraint for SAT solvers
14 votes

For the special case of k out of n variables true where k = 1, there is commander variable encoding as described in Efficient CNF Encoding for Selecting 1 to N Objects by Klieber and Kwon. Simplified:...

View answer
Find all items which are subsets of an item
3 votes

Your problem is the same one faced by SAT solvers who want to eliminate subsumed clauses from a CNF formula. Any clause $B$ that contains a superset of the literals of another clause $A$ in the ...

View answer
What are flops and how are they benchmarked?
1 votes

Apple has just proudly stated that their new mac pro will be able to give up to 7 teraflops of computing power. Flops stands for Floating Point Operations Per Second. How exactly is this benchmarked ...

View answer
Must a deadlock necessarily occur if the four conditions exist?
1 votes

If the four Coffman conditions exist, you have an existing deadlock. The circular wait condition guarantees at least two blocked processes exist, each waiting for a resource held by the other. The ...

View answer
Modeling the problem of finding all stable sets of an argumentation framework as SAT
Accepted answer
6 votes

Finding a stable argument set is equivalent to finding an independent set in the directed graph of argument attacks, with the added restriction that some member of the set must be adjacent to each ...

View answer
Converting (math) problems to SAT instances
15 votes

Unless you're translating mathematical problems to SAT instances as a learning exercise, your time will be much more fruitfully spent learning about satisfiability modulo theories. SMT will allow you ...

View answer
Alpha-Beta pruning in chess?
5 votes

What you are describing is unrelated to alpha-beta pruning. The tendency of fixed-depth minimax searches to badly underestimate or overestimate positional scores in dynamic situations is known as the ...

View answer
Tarjan's Strongly Connected Component algorithm
3 votes

1... On line 33 why is node.lowlink = min(node.lowlink, n.index) — shouldn't it be same as line 31: node.lowlink = min(node.lowlink, n.lowlink)? The code works either way. The two possibilities are: ...

View answer
Polynomial time reductions using binary search
1 votes

Is OPT = m? is a coNP decision problem. A "no" answer has a certificate verifiable in polynomial time, the certificate being a valid bin packing that uses fewer than $m$ bins. The same is true for ...

View answer
Proving NP Completeness of a subset-sum problem - how?
3 votes

The trick to the reduction is to use numbers to encode statements about the 3CNF formula, crafting those numbers in such a way that you can later make an arithmetic proposition about the numbers that ...

View answer
Implement queue with a linked list; why would it be bad to insert at the head and remove at the tail?
5 votes

Removing from the head and inserting at the tail are both constant time operations with a singly linked list, assuming head and tail pointers. Inserting at the tail is also constant time. But ...

View answer