Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
719 questions
0 votes
1 answer
37 views
Proof of variable elimination via resolution
I'm trying to do variable elimination by resolution in CNF SAT formulas. According to Wikipedia and other sources, the resolution rule states that $$ \dfrac{(p \lor a) \land (\neg p \lor b)}{(a \lor b)...
- 121
5 votes
2 answers
158 views
How is $\overline{SAT}$ not obviously in NP?
First of all, I do know that it is not known whether or not $\overline{SAT}$ is in NP. But to me, it clearly looks like it is in NP. Given a Boolean formula φ with n variables, we nondeterministically ...
- 91
1 vote
1 answer
145 views
How to model adversarial moves (e.g. chess) with Boolean Satisfiability?
I'm trying to solve the game of chess with a Boolean Satisfiability Sovler. For that, I implement a C/C++ program with some non-deterministic values, convert this program to a Boolean Formula (CNF) ...
- 165
0 votes
0 answers
48 views
Can the constants of FNV1A be computed for a specific set of strings to make it a perfect hash function?
I am hashing a bunch of strings made up of a finite number of known keyword strings (n many keyword strings). Here I want to generate a perfect hash s.t. each ...
- 187
1 vote
0 answers
58 views
Why is this probability $o(1)$ as $m \to \infty$ in a proof of a randomized algorithm for solving $k$-CNF ($k$-SAT) ? A mistake in a famous book?
This is about the proof of Lemma 5.13 in the well-renowned book Motwani R, Raghavan P. Randomized Algorithms. Cambridge University Press; 1995. Access with institutional login: link. (The lemma is in ...
- 11
0 votes
2 answers
109 views
Transform NAND gate to xorsat
Is it possibile to construct an xorsat problem with n variables that has as solutions only (0,1,...),(1,0,...),(0,0,...)? By dots, I meam the values of auxiliary variables, and these 3 vectors are the ...
4 votes
2 answers
236 views
Is Knuth's dancing cells XCC solver competitive against SAT/MILP/CSP solvers for exact cover problems?
Knuth's dancing links solver is featured prominently on the Wikipedia page of the Exact Cover Problem. A more recent version for exact cover with colors using Dancing cells was released by Knuth. This ...
- 225
0 votes
2 answers
98 views
How to transfer dividing calculation of binary integers to SAT problem or other NPC problems?
Is there any method to transfer dividing calculation between two binary integer numbers into a SAT problem or any other NPC problems? It seems that all the +-x/ calculations can be transferred into ...
0 votes
0 answers
87 views
What is a minimal NP-hard subset of SAT?
What is an example of a minimal NP-hard subset of SAT? For example, 3SAT is hard but a professor told me that "most" 3SAT instances are actually easy. Have we found a minimal subset, or at ...
- 23
0 votes
0 answers
62 views
Could this perspective of boolean satisfiability problem be used to find new algorithms?
Let's consider a boolean satisfiability problem with n variables in CNF form. We could consider that the n variables could represent a vector forming a integer between 0 and 2^n - 1. In that case, ...
- 11
0 votes
0 answers
34 views
Identifying the DMAC Literals Representing Internal Processes (Message Schedule, T1, T2, etc.) in SHA-256 CNF Conversion Using CGen Tool
When using the CGen tool to convert the SHA-256 algorithm into Conjunctive Normal Form (CNF), the input and output bits are represented by DMAC literals. However, I am specifically interested in ...
1 vote
0 answers
45 views
More Precise Interval Analysis
I am building an inference engine that uses interval analysis to compute variable bounds. Efficiency is very important in my case: I cannot use SMT solvers I cannot afford full enumeration, since ...
- 11
2 votes
1 answer
88 views
Hardness of this version of Dual Horn
I’ve been stuck on a problem while trying to prove that a restricted version of Dual Horn SAT is NL-hard. The input is a CNF formula such that (1) each clause has at most one negative literal (Dual ...
- 195
4 votes
0 answers
88 views
Smallest unions of shifts to cover the entire set?
Consider a subset $A\subseteq \{0, 1, 2, \dots, n - 1\}$. We define $A + i = \{(a + i) \text{ mod } n \mid a \in A\}$. For example if $A = \{1, 3, 4\}$ and $n = 5$, $A + 2 = \{3, 0, 1\}$. We want to ...
2 votes
0 answers
66 views
SAT directional resolution variable ordering
I've been researching directional resolution as mentioned here. After experimenting a bit, choosing a good variable ordering can make a big difference in the number of new clauses being generated. I'm ...
- 121