Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
659
questions
3
votes
1
answer
62
views
Reference asking: phase transition in SAT
This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate.
It has been experimentally observed (e.g. here) that when ...
- 33
1
vote
1
answer
758
views
What are the differences between symbolic execution and SAT solvers?
My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
- 184
-1
votes
1
answer
237
views
When does Gaussian elimination solve exact 1-in-3 SAT?
Terms:
A literal is a variable or its negation.
A clause is a set of literals.
An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
- 401
3
votes
1
answer
317
views
Having trouble understanding a proof of Mahaney’s theorem
I am reading a blog post of Lance Fortnow, which includes a proof of Mahaney's theorem.
I am not sure why $a’$ cannot be in between $w_i$ and $w_j$ in Case 1, and also why $a’$ cannot be in between $...
- 57
0
votes
1
answer
278
views
Maximum number of positive literals in 2SAT
MAX 2SAT is NP complete.
Instead of satisfying the maximum number of clauses, I have a fully satisfiable 2SAT formula and I want to have the maximum number of positive literals in the assignment (...
user102180
1
vote
1
answer
69
views
P=NP when number of inputs that give 1 is bounded by polynomial
Suppose there exists some NP-complete problem such that the number of inputs that gives 1 as an output is bounded by a polynomial; that is, if the problem is $f \colon \{0, 1 \}^* \to \{0, 1\}$, then, ...
- 57
1
vote
2
answers
215
views
Converting Mathematical Statements to SAT Formulas
Is it possible to write a mathematical statement (like Goldbach's conjecture, for example) as a nontrivial 3-SAT formula that is satisfiable iff that statement is true? iff it is false? iff it is ...
- 289
0
votes
0
answers
223
views
the correctness of 2-satisfiability problem algorithm by using implication graph
I learned finding a solution of 2-sat problem algorithm below.
The point are below
(1) when constructing the implication graph
(2) finding there is no occurrence of a variable x and its negation x' ...
- 11
1
vote
1
answer
129
views
building a polynomial algorithm that solves SAT when given a polynomial TM that solves SAT on two formulas
Here's the question:
Assume there exists a polynomial time machine $M$ that receives two formulas $\varphi_1,\varphi_2$ and satisfies the following:
If $\varphi_1 \in \mathrm{SAT}$ and $\...
2
votes
0
answers
44
views
Names of specific SAT variants
I enjoy reading research on satisfiability, but sometimes it's easier to find relevant information when you know the names of the variants.
Example:
All the clauses are width 3 and must have ...
user102180
0
votes
1
answer
81
views
Turing reducibility of 2 versions of the satisfiability problem
I need help with this problem.
There are 2 versions of the satisfiability problem:
[1] decision version: determine whether an arbitrary formula f is
satisfiable or not
[2] search ...
- 5
0
votes
1
answer
75
views
Reducibility of 2 boolean satisfiability problems
I beg some help with this problem.
There are 2 boolean satisfiability problems.
Problem $A$: Determining whether an arbitrary formula of size $n$ is $satisfiable$.
Problem $B$: Determining ...
- 5
3
votes
2
answers
2k
views
Unique 3SAT to Unique 1-in-3SAT
Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment.
It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such ...
user102180
1
vote
1
answer
161
views
Unique 1-in-3 SAT
Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment.
I know the value of each bit of the unique assignment because it was made from a binary ...
user102180
-2
votes
2
answers
383
views
Prove or Disprove, 3SAT ≤p 2SAT, then P = NP
I know that 3SAT is in NP and 2SAT is in P. And 2SAT can reduce to 3SAT just says 3SAT is strictly harder than 2SAT, so I don't think this proves P = NP, but it doesn't seem to disprove it either.
- 1
10
votes
2
answers
3k
views
What is wrong with this simple proof of P=NP?
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 341
2
votes
1
answer
63
views
Programming in Propositional Logic article notation question
I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section):
I don't understand what $[v,i]$...
2
votes
1
answer
370
views
MAX 2-SAT is polynomial time reducible to 2-SAT?
I know that 2-SAT is solvable in polynomial time and 2-SAT is NP-Hard.
I have issue about this statement:
MAX 2-SAT is polynomial-time reducible to 2-SAT. Can you explain to me how reduction looks ...
- 133
2
votes
1
answer
800
views
Time complexities of state-of-the-art SAT solvers with respect to length of the formula
I am learning about DPLL and CDCL SAT solvers, and I know that they have time complexity exponential to the number of variables.
If I am not mistaken, one of the reasons why most believe P does not ...
- 145
1
vote
1
answer
682
views
Use 2SAT to show that an implication graphs must have a cycle if it's not satisfiable
Using 2SAT and implication graphs, how could I prove the following properties of implication graphs:
Suppose there is a directed path between literals l1 and l2 in G_φ. Then there is also a directed ...
- 352
3
votes
1
answer
430
views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
3
votes
1
answer
123
views
Clarification on "clause learning" in DPLL algorithm
I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
- 687
2
votes
0
answers
23
views
Flip Output of SAT problem [duplicate]
Why cant I Just create a TM A that runs a NTM B with a formula to compute the SAT Problem and Just Flip its Output. So when the Input NTM B Returns true (formula is satisfyable) the TM A Return false.
- 121
3
votes
1
answer
467
views
Special Monotone SAT problem: NP complete?
Say we have the set $X=\{ x_1, x_2, \dots \}$ of variables. Then we consider the following problem: Is the formula
$$\bigwedge_{(a,b,c) \in A}(a \vee b \vee c) \wedge \bigwedge_{(a,b,c) \in B}(\neg a ...
- 143
4
votes
2
answers
1k
views
Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT
Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a ...
- 161
6
votes
2
answers
390
views
An Exact Method for Solving Small Instances of XORSAT
I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
- 63
2
votes
0
answers
88
views
Class of languages recognizable by n-bit formulas of size at most $T(n)$
A Boolean (combinatoiral) circuit is a labeled (with the labels: AND, OR, NOT, IN, OUT), directed, acyclic graph, that satisfies:
fan-in=2 for the AND and OR nodes
fan-n=1 for the NOT nodes
fan-...
- 161
0
votes
0
answers
117
views
Give me ideas for an undergraduate final year math project about Boolean Satisfiability and SAT solvers
Context
I am a student starting an undergrad math project.
I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material.
I have 13 weeks ...
- 111
1
vote
0
answers
62
views
Are there any resources or forums online for helping me understand TAOCP?
Context
I am doing an undergrad math project that involves exploring Donald Knuth's "TAOCP, Volume 4, fascicle 6: Satisfiability".
I am having trouble parsing some of this material.
Surely ...
- 111
2
votes
0
answers
49
views
Boolean matrix / satisfiability problem [duplicate]
Let $M$ be an $m\times n$ matrix with all elements in $\{1,0\}$, $m >> n$. Let $\mathbf{v}_0, \ldots, \mathbf{v}_n$ be the columns of $M$.
I want to find all sets of columns $S = \{\mathbf{v}_{...
- 121
2
votes
1
answer
209
views
Encoding set of At-Most-One constraints as a MAX-SAT problem
Assume a set of variable $V$ = $\{v_1,...,v_m\}$.
Given total $n$ at-most-one (AMO) constraints (at most one element in a given set is true) set [of the below form], over the variable set $V$,
$$ AMO \...
- 933
1
vote
1
answer
477
views
Integer programming to MAX-SAT translation
Reading A Comparison of Methods for Solving MAX-SAT
Problems, I can see that a MAX-SAT problem can be translated to an integer programming (IP) problem.
Definition of MAX-SAT [Wikipedia]:
The ...
- 933
4
votes
2
answers
432
views
Is it feasible to solve this subset cover problem with SAT solver?
The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:
if $S \subseteq \mathcal{S}$ then $|S|=6$;
for any $A \subseteq \{1,...
- 568
3
votes
1
answer
170
views
CNF satisfiability with a bound on number of clauses
Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
- 131
4
votes
2
answers
337
views
Are SAT problems with at most two false clauses NP-complete?
Is the problem of deciding whether a SAT instance, where at most two clauses are false (that is, any given variable assignment will either lead to all clauses being true, all but one, or all but two), ...
- 43
2
votes
1
answer
125
views
Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)
I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." ...
- 123
5
votes
2
answers
470
views
checking '<' for two binary numbers in a cnf-formula
I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf:
Lets say n and m are two-digit ...
- 53
1
vote
1
answer
240
views
Find a truth assignment of 2SAT that has the most number of true variables?
Given a 2SAT instance in CNF where each clause has at most two literals. Let $m$ be the number of clauses and $n$ be the number of variables et let $k$ be a positive number.
Question: Is there a ...
- 1,046
4
votes
1
answer
592
views
Are SAT problems with at most one false clause NP-complete?
Is the problem of deciding whether a SAT instance, where at most one clause is false (that is, any given variable assignment will either lead to all clauses being true, or all but one), is satisfiable ...
- 43
3
votes
1
answer
511
views
How to encode reachability in a graph with walls as a SAT problem
Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
- 155
3
votes
1
answer
735
views
Practical hard 3-sat instances
The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
- 33
-1
votes
2
answers
263
views
A question about NP and coNP
It is an open question if NP $\neq$ Co-NP but if the conjecture were proved, this would mean that P $\neq$ NP
because P is closed under complement.
Now a fact that fails to enter my head is the ...
- 1,063
1
vote
0
answers
780
views
Min-Ones-2-SAT getting to vertex cover
In the Min-Ones-2-SAT problem, we are given a 2-CNF formula φ and an integer k, and the objective is to decide whether there exists a satisfying assignment for φ with at most k variables set to true....
- 111
1
vote
1
answer
154
views
Is inverse CNF polynomial?
Suppose we are given a CNF formula $F$ with $n$ variables and $m$ clauses. The question is whether we can represent $\lnot F$ as a CNF formula with the number of clauses polynomial in $n$ and $m$?
- 952
7
votes
1
answer
852
views
Random restarts for unsatisfiable instances
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
...
- 386
1
vote
1
answer
655
views
Is properly quantified 3SAT complete for PSPACE and all PH levels?
I know 3SAT is NP-complete and QSAT is PSPACE-complete. However, is it true that
$$\exists X_1 \forall X_2 \cdots Q_k X_k \colon \varphi(X_1, \ldots, X_k)$$
is complete for $\Sigma_k$, the ...
- 709
3
votes
1
answer
127
views
High-dimensional geometry and P vs. NP
Background: Recently, I obtained the following equivalent problem to SAT. We are given as input a CNF formula with $n$ variables and $m$ clauses. Suppose we have an $n$-dimensional hyper-cube centered ...
- 952
0
votes
2
answers
348
views
Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?
I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:
elimination of equivalence
Elimination of ...
4
votes
1
answer
3k
views
CLIQUE $\leq_p$ SAT
i'm trying to reduce CLIQUE to SAT:
Given: Graph G=(Vertices V, Edges E) and $k \in \mathbb{N}$
Output: Formular F such that if G contains a complete subgraph of size k, the formular is satisfiable (...
- 185
0
votes
1
answer
121
views
A doubt on converting NOT gate to CNF formula
For a NOT gate if $x_1$ is input and $x_2$ is the corresponding output, I see the equivalent CNF (conjunctive normal form) is $(x_1 \lor x_2) \land (\overline x_1 \lor \overline x_2)$.
My ...
- 229