Kyle Jones
  • Member for 10 years, 1 month
  • Last seen more than a week ago
  • Seattle, WA
What is the precise definition of Random K-SAT?
14 votes

[Edited for clarity] The most widely used definition in the research literature is the one that requires exactly k distinct variables per clause, and no duplicate clauses. If you relax the distinct ...

View answer
Starting SAT solver papers
9 votes

Start with a good survey paper. It's easy to attack the subject piecemeal and get confused by different names in the literature for the same techniques and the same name used for different techniques....

View answer
How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?
Accepted answer
7 votes

Let $m$ be the number of pigeons and $n$ be the number of holes. Let the propositional variables $B_{i,0}$ ... $B_{i,log(n)}$ encode the binary representation of $j-1$ if the $i$th pigeon is put into ...

View answer
Conversion between k-SAT and XOR-SAT
Accepted answer
6 votes

If all XOR relationships between variables in CNF formulas could be detected in polynomial time, then this would allow the solution of UNAMBIGUOUS-SAT in polynomial time. By the Valiant–Vazirani ...

View answer
Eliminating clauses from a CNF formula based on their unsatisfying truth assignments being covered by some other clause
Accepted answer
5 votes

What you're describing is called subsumption; it is a standard CNF simplification technique for SAT solvers. None of the operations involved is worse than quadratic to either the number of variables ...

View answer
Translating pure literal elimination into rup
1 votes

Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions. But ...

View answer
Abstract high-level framwork for #SAT
0 votes

Starting with the transition system for DPLL in definition 1 in the paper, add a state corresponding to the condition: $M \models F$ and no $l$ that appears in $F$ is undefined in $M$. The transition ...

View answer
Is there an algorithm for 3x3 sudokus without backtracking?
Accepted answer
-3 votes

Solving a Sudoku puzzle is equivalent to deciding whether there is a valid graph vertex coloring using $k$ colors, where $k = 9$ in your $3 \times 3$ Sudoku instance. The graph coloring problem is ...

View answer