Kyle Jones
  • Member for 9 years, 10 months
  • Last seen this week
  • Seattle, WA
An Exact Method for Solving Small Instances of XORSAT
Accepted answer
2 votes

If your formula has $n$ variables, for each value of $k$ from 1 to $n$, add an exactly-$k$ cardinality constraint to your SAT instance and then run a SAT solver on each result. The solver will only ...

View answer
What is the difference between masking and tolerating failures?
2 votes

The source of your misunderstanding may be that you think the excerpt contains a list of methods to handle system failures that are mutually exclusive. Masking and tolerating failures often happen ...

View answer
How Tarjan algorithm work for the 2-SAT
2 votes

a 2-CNF formula is satisfiable if and only if there is no variable that belongs to the same strongly connected component as its negation. But I don't find any reason for the right to left direction. ...

View answer
What are known 3SAT to 2SAT reductions?
Accepted answer
2 votes

You seem to be asking about logically equivalent 2CNF functions rather than equisatisfiable ones. Not all Boolean formulae can be expressed as 2CNF formulae. Your example $(a \oplus b \oplus c)$ is ...

View answer
Does SAT always have short analytic proofs?
2 votes

It is known that proofs of the unsatisfiability of pigeonhole problems must be at least length $2^{n^\epsilon}$ when the resolution proof system is used. $\epsilon$ depends on the difference between ...

View answer
What is the complexity of determining Satisfiability of a CNF containing both Horn and Dual Horn clauses?
Accepted answer
2 votes

3-CNF formulas contain a mixture of only Horn and dual-Horn clauses. 3-SAT, the Boolean satisfiability problem over 3-CNF formulas, is known to be NP-complete. So it is unlikely that the ...

View answer
How to adapt DPLL to solve HORNSAT?
2 votes

Horn formulas are always satisfiable unless there is at least one unit clause that contains a positive literal. (Otherwise assigning false to all the variables guarantees the formula would be ...

View answer
GOTO vs. including line in loop - will it affect efficiency?
2 votes

Modern languages are heavily optimized, so much so that it is hard to predict if minor code changes will make an algorithm run faster. In particular with matrix math, whether the language ...

View answer
Modeling tiling problems as SAT problems
2 votes

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

View answer
Best improvements to do to the DPLL SAT algorithm
Accepted answer
2 votes

The most improvement with the least effort will come from adding rapid random restarts to your solver. DPLL is known to exhibit heavy-tailed behavior, producing both short and long search times for ...

View answer
Upper bound for #Monotone k-SAT
Accepted answer
2 votes

A $k$-SAT instance over $n$ variables, monotone or otherwise, has at most $2^n - 2^{n-k}$ solutions. This is simply the number of possible settings of the $n$ variables minus the least number of ...

View answer
Does the memory get unallocated when program exits?
Accepted answer
2 votes

When you run your program its memory allocations take the form of page allocation requests to the operating system. When your program terminates, the operating system notices and returns all the ...

View answer
Proving "QUESTION" is NP-Complete by reduction from n-variable 3SAT
2 votes

The reduction is straightforward, but what's likely tripping you up is that while 3CNF clauses seem to describe what's needed for a satisfying assignment, what they do more directly is describe what ...

View answer
How does a hard drive knows what bit is the beginning of of a byte/word?
Accepted answer
2 votes

Simplified, the operating system sees disk storage as a randomly accessible set of sectors, each sector containing some fixed number of bytes. The OS asks the disk controller for a sector using some ...

View answer
Difference between the two regular expression
Accepted answer
2 votes

Your regular expression (a+ba*b)* won't match the string a which contains zero b's, an even number. It also won't match the strings bb or bbbb, because the expression requires one or more a's before ...

View answer
Radix sort and changing bases
Accepted answer
2 votes

The asymptotic runtime ignores access times for the digits. On typical hardware a base 256 number can be manipulated faster than extracting base 10 digits from the same number. If you have multiple ...

View answer
Algorithm for finding all the combinations on a boolean array
2 votes

The pattern you're trying to match is regular and can be matched by the regular expression 1(0?1)*. A good strategy would be to convert the binary array to a string and do regular expression matches ...

View answer
Algorithm for Dynamic Client Side Throttling
2 votes

Only the server can accurately determine what its current load is, and thus how much more work it can handle or when it might be able to handle more work in the future. This is why load balancing and ...

View answer
Strongly connected components on a DAG
2 votes

I know of no convention; the right result depends entirely on what you want to do with the result. As an example, if you're trying to use strongly connected components to find satisfying assignments ...

View answer
Basic question about backjumping in SAT solvers
Accepted answer
2 votes

The intervening assignments between the current assignment and the backjump point might have been arrived at via considerable backtracking and backjumping themselves and it would be wasteful to repeat ...

View answer
Reduction of Circuit Satisfiability to CNFSAT
2 votes

The exponential blowup when converting circuits to conjunctive normal form is avoided by introducing new variables to represent the output of each sub-circuit plus a simple set of rules represent each ...

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
How can we reduce variables when converting from 3-SAT to 4-SAT?
2 votes

The paper Effective Preprocessing in SAT through Variable and Clause Elimination covers the variable elimination techniques used in Minisat. Broadly, variables can be eliminated by Substitution, in ...

View answer
Is Max 3-SAT W[1]-hard?
1 votes

The W hierarchy consists of classes of decision problems. The decision versions of MAX-SAT problems are just slightly disguised SAT problems. For example, to transform the decision problem "is ...

View answer
Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?
1 votes

I don't think such a 100-variable 3-SAT problem exists. PPSZ can solve satisfiable 3-SAT problems in ~ $O(1.321^n)$, which equates to well under 2 trillion decisions for a 100-variable 3-SAT problem. ...

View answer
How can you apply dynamic connectivity problem to digital photos?
Accepted answer
1 votes

The problem manifests when maintaining connectivity data either in edges or objects within the image. For machine vision you might want to increase the reliability of an edge detection algorithm by ...

View answer
Is possible applying virtual memory with cloud disk (cloud storage) instead of local disk (SSD/HDD)?
Accepted answer
1 votes

Thirty years ago Sun Microsystems was selling diskless workstations that accessed all mass storage (root, user directories, virtual memory / swap) over 10Mbit Ethernet, which is considerably slower ...

View answer
Computational complexity of dividing a set of constraints into a minimum number of satisfiable clusters
1 votes

I think your problem is NP-hard for k = 1 since that is equivalent to SAT, but it is in P for k > 1. For example, a SAT instance can be easily decomposed into two satisfiable subformulas. Go from ...

View answer
Is there CIRCUIT-SAT algorithms that slightly depends on gates count?
1 votes

Yes, such an algorithm exists, but it is the same algorithm used for SAT solving in general. While the Tseytin extension variables associated with gates do appear in the CNF transformation of the ...

View answer
What would be the practical consequences of ZPP=exptime
1 votes

If ZPP = EXPTIME then NP $\subseteq$ ZPP, which implies NP $\subseteq$ BPP. As described in Russell Impagliazzo's informal paper "A personal view of average-case complexity", we would be ...

View answer