Kyle Jones
• Member for 9 years, 10 months
• Last seen this week
• Seattle, WA

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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