Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
485
questions
0
votes
0answers
14 views
3SAT and directed graph
Given a 3SAT instance (a Boolean expression in three conjunctural normal form), we draw a directed graph, where for each Boolean variable $x_{i}$ we have the nodes $x_{i}$ and $!x_{i}$; for each ...
1
vote
1answer
37 views
Universal Quantifiers in QBFs
I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
1
vote
1answer
29 views
Is there an algorithm for reducing CNFs further
I have a boolean formula in conjunctive normal form (CNF):
$(a\vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (x \vee y)$
I know that this can be simplified to:
$(a\vee b)\wedge (x \vee y)$.
a) Is ...
1
vote
1answer
30 views
algorithm for checking satisfiability
In order to prove that SAT is in NP, I need to come up with a polynomial time verfier (an algorithm). The Cooks Levin Theorem uses a non-deterministic Turing machine but that's not what I am looking ...
2
votes
1answer
83 views
Complexity of specific cases of MAX2SAT
I know that MAX2SAT is NP-complete in general but I'm wondering about if certain restricted cases are known to be in P. Certainly the languages
$L_k:=\{ \phi \,|\, \phi\,\text{is an instance of 2SAT ...
3
votes
1answer
39 views
Is MAX-averageSAT a well-known problem?
Is there any variant of the Boolean SAT or Max-SAT problem that has a flavor of maximizing or minimizing the average of the weights of the satisfied clauses of a WCNF formula? Any literature on an ...
0
votes
1answer
44 views
NP-Complete Problem and Polynomial Hierarchy
I have tried to search the internet to check if the following is correct:
If $\sum_{2}$ contains a NP-Complete problem then PH collapses to NP: $PH=NP$
For example if $SAT\epsilon\sum_{2}$ than: $PH=...
0
votes
0answers
14 views
Global-input-local-output p-time algorithms
Are there polynomial-time algorithms whose input is global but output is local in nature? What I have in mind is a problem instead of an algorithm. Itās the satisfiability (SAT) problem. Each clause ...
3
votes
1answer
130 views
How many clauses are required for SAT to be NP-hard in CNF formulas?
It is not hard to see that SAT for a CNF formula with $n$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $...
0
votes
1answer
33 views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
2
votes
2answers
69 views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
2
votes
0answers
26 views
Reducing Dominant Set Problem to SAT
I am trying to solve a problem and I am really struggling, I would appreciate any help.
Given a graph $G$ and an integer $k$ , recognize whether $G$ contains dominating set $X$ with no more than $k$ ...
1
vote
1answer
75 views
Is Monotone 3-SAT with exactly 3 distinct variables untractable?
I have given the following SAT variation:
Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated....
2
votes
3answers
65 views
Why isn't SAT in coNP?
I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?).
But I'm missing why the following machine doesn't turing recognize the complementary of SAT:
Given a ...
0
votes
1answer
40 views
MAXSAT using dpll algorithm?
It's possible to return from a dpll algorithm M as maximum for MAX-SAT problem?:
I have a sample:
https://gist.github.com/davefernig/e670bda722d558817f2ba0e90ebce66f
we can modify recurrency to return ...
11
votes
3answers
2k views
Are there competitions for integer programming?
Are there competitions for integer programming like there are for SAT and MAXSAT?
2
votes
1answer
176 views
Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset
I am working on a problem defined as the following
Given a set of $n$ elements called $R \subseteq \mathbb{N} \times \mathbb{N}$ and numbers $Z,G \in \mathbb{N}$, where $Z$ is a measure of our ...
-1
votes
1answer
37 views
Does 2SAT contained in SAT?
Is it true that $2 S A T \subseteq S A T ?$ and in general is $k S A T \subseteq S A T $ where k is any positive integer is true?
Thanks.
0
votes
0answers
26 views
CNF encoding of additions
I have $m$ equations of the following form:
$$x_1+x_2+\cdots+x_n=s,$$
where each variable is either 1 or 0, and the total number of variables is $m\approx3{,}000$. So Iām thinking of modeling each ...
3
votes
1answer
48 views
Complete resolution rule for 1-in-k SAT
In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal.
(A or B or C) and (!A or D ...
1
vote
3answers
162 views
Counting the number of satisfied models - given mathematical constraints
Question
There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...
3
votes
1answer
32 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 ...
1
vote
1answer
56 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 ...
0
votes
1answer
44 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 ...
0
votes
0answers
16 views
Translating running times of $3$-coloring to $k$-$SAT$ complexity
Suppose there is an $O(f(n))$ algorithm for $3$-coloring a graph on $n$ vertices what does it translate to in terms of time complexity for solving $k$-$SAT$ with $m$ clauses?
3
votes
1answer
88 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 $...
0
votes
1answer
31 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 (...
1
vote
1answer
60 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, ...
1
vote
2answers
88 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 ...
0
votes
0answers
18 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' ...
1
vote
1answer
46 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
0answers
25 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 ...
1
vote
1answer
65 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 ...
1
vote
1answer
62 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 ...
1
vote
0answers
54 views
CircuitSAT to 1-in-3SAT
This question follows
Unique 3SAT to Unique 1-in-3SAT
Consider an AND gate such that (A ā§ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables.
$$
(A āØ B āØ \overline{...
2
votes
2answers
168 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 ...
1
vote
1answer
27 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 ...
0
votes
1answer
91 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.
10
votes
2answers
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 ...
2
votes
1answer
42 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
1answer
72 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 ...
1
vote
1answer
73 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 ...
1
vote
1answer
87 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 ...
2
votes
1answer
41 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
1answer
59 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 ...
2
votes
0answers
22 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.
2
votes
1answer
68 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 ...
4
votes
1answer
150 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 ...
5
votes
2answers
263 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 ...
2
votes
0answers
85 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-...
