Questions tagged [sat]
SAT stands for the Boolean satisfiability problem.
330
questions
0
votes
0
answers
22
views
How often can a clause cause a conflict?
This question is about DPLL+CDCL algorithms. How often can a clause cause a conflict?
I want to use a specific algorithm. Assume a DPLL+CDCL SAT solver using a fixed variable order. Variables and unit ...
- 549
-1
votes
0
answers
29
views
corresponding resoving and arbitary resolving
Notations:
$$C_x \otimes C_{\bar{x}} = V_1 \lor \ldots \lor V_a \lor W_1 \lor \ldots \lor W_b$$
$$ \text{ where } C_x = x \lor V_1 \lor \ldots \lor V_a \text{ and } C_{\bar{x}} = \bar{x} \lor W_1 \lor ...
- 315
5
votes
1
answer
146
views
Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?
I have a question regarding the Conflict-Driven Clause Learning (CDCL) algorithm applied to an unsatisfiable CNF formula $F$.
Specifically, can all the conflict clauses learned by the CDCL algorithm ...
- 315
16
votes
2
answers
1k
views
Is there a SETH (Strong Exponential Time Hypothesis) for CSP (Constraint Satisfaction Problem)?
The Constraint Satisfaction Problem I mentioned is similar to CNF-SAT: A variable can take values from some finite domain $D$ where $|D| = d$. A literal of variable $x$ is an expression of the form $x\...
- 163
6
votes
0
answers
84
views
Certifying the promise in hard promise problems
Do we happen to know of any promise problems where the problem is both conditionally hard (say, NP-hard) while simultaneously being able to certify that the instance satisfies the given promise?
For ...
- 801
0
votes
0
answers
46
views
Using Simplex for Difference Logic
I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures.
Clearly, in this case, all constraints of ...
- 161
4
votes
1
answer
84
views
Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. I am intersting in finding the minimal width of some certain ...
- 315
12
votes
1
answer
229
views
Complexity of 1-or-3-in-3-SAT (odd-3-SAT)
Consider a 3-CNF formula $\Phi$, i.e., a conjunction of clauses of 3 literals. I call odd-SAT (or 1-or-3-in-3-SAT) the problem of checking whether there is an assignment of the variables such that ...
- 8,896
7
votes
1
answer
402
views
What kind of resolution is CDCL corresponding to?
For an unsatisfiable CNF instance, CDCL will return a resolution refutation.
My question : what kind of resolution does it return? tree-like, regular or general?
- 315
1
vote
0
answers
72
views
Using a certificate in the proof of NP hardness
Say I wanted to determine that the problem of membership in some language $L \subseteq \{0, 1\}^*$ is NP-hard. Say that I have a reduction $r: \{\text{set of quantifier free formulas} \rightarrow \{0,...
- 21
1
vote
0
answers
124
views
Can "dense" SAT instances be solved in time $o(2^n)$?
By "dense" I mean instances in which the ratio of variables to clauses is below the critical threshold $2^k\ln2−\frac{(1+\ln2)}2+\epsilon_k$ for $k$-SAT. For general SAT, however, I suppose ...
- 245
7
votes
1
answer
152
views
Conversion between NP certificates
This might be a well-known fact, but I can't convince myself of whether this is true.
Suppose I have some NP language and two different verifying procedures V and V' for L. For any x in L, is it the ...
- 801
1
vote
1
answer
45
views
Efficient algorithm/ implementation to compute Transitive Closure of a Rule with respect to a Relationship
(Recalling some) Definitions:
Fix a finite collection of finite sets: $A_1,\ldots,A_k$. Then relationship $R\subseteq A_1 \times A_2 \times \ldots\times A_k$. (Remark: $A_i$'s need not be distinct.)
...
- 111
1
vote
0
answers
82
views
$NP\subseteq P/poly\implies PH\subseteq P/poly$ [closed]
We know if $NP\subseteq P/poly$ then $PH=\Sigma_2$ Then We want to show that $\Sigma_2-SAT\in P/poly$. Now $$\phi\in \Sigma_2-SAT\iff \exists\ x\in\{0,1\}^{p_1(n)}\ \forall\ y\in \{0,1\}^{p_2(n)},\ \...
- 288
0
votes
0
answers
97
views
When the tree-like resolution size is the same with general(regular) resolution size？
Background:
For an unsatisfiable SAT formulas, the length of a resolution refutaion means the number of clauses in it.
It's well known that there exist exponential separation between tree-like and ...
- 315
2
votes
0
answers
91
views
What kind of solver should I use for this hypergraph problem?
I have to list the solutions to the following hypergraph problem:
There is a set of nodes, linked by edges that are 2-to-1 and bidirectional. The possible directions are either direct: 2 sources and 1 ...
- 8,598
3
votes
0
answers
42
views
Can you compute Shannon expansion of a Boolean formula more efficiently by using a QBF solver?
Maybe this is not enough research level, but I've been scratching my head on it for a while...
I'm interested in the Shannon expansion of an existentially quantified Boolean formula of the form:
$$ \...
- 1,588
0
votes
0
answers
154
views
What's the connection between branchwidth and treewidth
I understand that treewidth and branchwidth are essentially equivalent for a fixed graph, given that $branchwidth(G) = Θ(treewidth(G))$.
However, my question pertains to a specific case involving ...
- 315
0
votes
1
answer
139
views
Sources that prove solving 2-SAT with DP takes linear time
Would anyone have any sources that describe/an explanation of how solving 2-SAT using dynamic programming takes a linear amount of time? Can't seem to find a text that proves it in detail/formality. ...
1
vote
0
answers
172
views
What advancements in SMT solvers have contributed to progress in the field of theoretical computer science?
SMT solvers use first-order logic on top of SAT solvers with boolean logic. For example, CVC4 is an SMT solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays, ...
- 181
13
votes
2
answers
2k
views
Algebraic equivalent of SAT?
Starting with a simple observation. If $x,y\in\{0,1\}$, then the arithmetic product $x\cdot y$ corresponds to the logical conjunction if we interpret $1$ as true and $0$ as false.
But then, for a ...
- 1,588
0
votes
1
answer
67
views
Require Hamming weight in CNF
I have a SAT problem in conjunctive normal form that I’d like to solve, but I need to add one more condition: for the existing variables $x_1,\ldots,x_n$ the Hamming weight is $k$. (It would be ok to ...
- 1,737
0
votes
1
answer
80
views
Regarding UNSAT bechmark of SATLIB found as SAT instance
I found the Satisfiable assignment to one of the UNSAT [SATLIB benchmark][1] instance, specifically uuf50-01.cnf as below answer:
[1, 2, 3, 4, -5, -6, -7, -8, 9, 10, -11, 12, 13, 14, -15, -16, 17, 18, ...
- 11
0
votes
0
answers
116
views
3SAT instances where no assignment fails to satisfy more than one clause: do they eixst, and what complexity class do they belong in?
Title says it all. I am curious of the 3SAT problem but limited to instances where only one clause is left unsatisfied by any literal assignment.
Do such problems exist, and if they do, what is it ...
- 101
1
vote
1
answer
72
views
Running time of SAT and other EXPTIME algorithms [closed]
I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
- 11
0
votes
1
answer
203
views
list of 3-CNF formula that can be solved in polynomial time
Suppose i want to program a 3-SAT solver. I want my solver to first check whether a formula is in the list of 3-CNF that currently known can be solved in polynomial time before resorting to brute ...
- 101
-2
votes
1
answer
581
views
Solving 3-SAT in O(n^6)?
There's an algorithm (published on GitHub) which is claimed to solve any 3-SAT formulation in polynomial time with a complexity of max O(n^6). I would usually brush claims like this away, but having ...
- 73
2
votes
1
answer
152
views
Short UNSAT Certificates for X3SAT
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 549
1
vote
0
answers
341
views
proof that 2-SAT is P-hard [closed]
i'm doing university work about the 2-sat problem and it is asked why 2-sat is p-hard. We discussed that 3-sat is np-hard and proved this by reduction from cnf-sat to 3cnf-sat. for my work the ...
- 11
2
votes
1
answer
210
views
Complexity of the Complete (3,2) SAT problem?
A complete $k$-CNF formula is a $k$-CNF formula which contains all clauses of size $k$ or lower it implies.
Deciding the satisfiability of a complete $k$-CNF formula is clearly a tractable problem ...
- 1,109
0
votes
2
answers
123
views
Find whether a 3CNF formula with every clause having either all the variables negated or all the variables non-negated is satisfiable
Given a 3CNF formula $\phi$ with the condition that, for every clause of $\phi$, either all the variables are negated or all the variables are non-negated. For example, some allowed clauses are $(x_1\...
2
votes
1
answer
303
views
The complexity of 3SAT
It is well known that 3SAT remains NP-complete if every variable occurs exactly twice positively, exactly once negated.
then, does 3SAT remain NP-complete if every variable occurs exactly once ...
- 89
6
votes
1
answer
143
views
Complexity of maximizing the number of models in a parametric formula
Let $F(x,y)$ be a propositional formula where $x$ and $y$ are vectors of Booleans. We want to maximize over $x$ the number of models of $F$ over $y$. As a decision problem, this becomes: given $F(x,y)$...
- 1,122
0
votes
1
answer
149
views
SAT to k-in-3-SAT reduction
Given a 3-SAT clause. Is there a way to convert 3-SAT to k-in-3-SAT such that:
The number of new variables introduced are less than the number of clauses (without adding dummy clauses etc.)?
The ...
- 468
-1
votes
1
answer
159
views
Polynomially solvable 3-SAT problem instances [closed]
Given the 3-SAT problem with $v$ variables and $c$ clauses:
Is there a clause to variable ratio for which the 3SAT problem is 'easy' i.e. solvable in polynomial time?
We are assuming the 3-SAT ...
- 793
6
votes
2
answers
265
views
Is there an Upper Bound on Number of Redundant Clauses in a satisfiable $3-SAT$?
For a non-empty $3-SAT$ with $n\geq3$ variables and $T\geq1$ non-identical non-degenerate clauses $C_i$:
$$S=C_1 \wedge \ldots \wedge C_T$$
where a non-degenerate clause is one containing $3$ unique ...
- 171
1
vote
1
answer
161
views
3-SAT runtime if an optimal order to eliminate possible solutions is known
As a mental exercise I have been playing around with the 3-SAT problem, but I am having difficulty proving or disproving the usefulness of a current idea that I am playing around with.
My current ...
1
vote
1
answer
239
views
Can this NP-hardness proof for Super Mario Brothers (and other games) be simplified?
In "Classic Nintendo Games are (Computationally) Hard", a generalized framework based on reducibility of 3-SAT for proving NP-hardness of classic Nintendo games is presented, and several ...
- 11
9
votes
1
answer
306
views
Does Horn SAT (Horn formula in CNF) have an integral polytope?
In some ways, my question is related to this: Is the matching polytope integral?
Matching and Horn-SAT are both polynomial time solvable.. So I wonder if there is a Horn polytope, similar to the ...
- 113
1
vote
1
answer
135
views
Lower bound for proving a random 3-SAT formula is unsat?
For a random 3-CNF formula with n variables and m clauses, assume this formula is unsat, what is the lower bound for proving it to be unsat?
Some results posted in Lower bounds for random 3-SAT via ...
- 181
0
votes
1
answer
216
views
Lexicographic Boolean satisfiability
Maximal Satisfying Assignment (Lexicographic Boolean satisfiability / LexMaxSAT), the problem of finding the lexicographically maximum x_1, . . . , x_n ∈ {0, 1}^n that satisfies Boolean formula φ, or ...
2
votes
0
answers
100
views
Resource on phase transition in MAXCUT problems
Could anyone suggest reading materials on phase transition in MAXCUT problems other than [1]? Thanks.
Ref:
Coppersmith, Don, David Gamarnik, Mohammad Taghi Hajiaghayi, and Gregory B. Sorkin. "...
- 653
-2
votes
1
answer
68
views
Linear Integer Arithmetic Satisfiability with Three Literals [closed]
I'm stuck on trying to find an unsatisfiable conjunction of the form $a \wedge b \wedge c$ where:
$a \wedge b$ is satisfiable
$a \wedge c$ is satisfiable
$b \wedge c$ is satisfiable
$a, b, c$ are ...
- 99
2
votes
1
answer
138
views
Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)
I would like to check a sort of SMT formulas with two quantifiers where universal variables range over finite/bounded integer domains. An example formula is
$$\exists x \forall y ((y \ge 1 \land y \le ...
- 75
2
votes
0
answers
101
views
Resource on the Lee-Yang zeroes of the partition function of random $3$-SAT problems
Could anyone point me to the representative papers on the study of the Lee-Yang zeroes of the partition function of random $3$-SAT problems?
- 653
8
votes
2
answers
257
views
Are there analogous works to PPSZ algorithm for #P?
The PPSZ algorithm tells us that we can do SAT-solving for
$k-$CNF in time at-most $2^{1-(1-o(1))\frac{\pi^2}{6k}}$.
My question is that do we know such results for counting problems in class #P too ? ...
- 706
0
votes
0
answers
68
views
Asymptotically sub-optimal but provably optimal algorithms in a finite range for NP-Hard problems?
Given a formula in propositional logic with $100$ variables. We know that there can be no SAT-checking provably faster than $O(2^n)$, unless P=NP. Now let's say I could find an algorithm which does ...
- 706
0
votes
1
answer
181
views
Comparing SAT to MCSP reduction class separations and faster SAT class separations?
Assume $SAT$ is in $QuasiP$. We immediately infer $NQuasiP=QuasiP$ and $EXP=NEXP$. From https://people.csail.mit.edu/rrw/easy-witness-nqp.pdf we infer $NQuasiP$ is not in $P/poly$ which implies $...
- 12.8k
1
vote
0
answers
30
views
Clauses structure as quenched random matrix for random $k$-SAT problems
In the Section III of Statistical mechanics of the random K-SAT model, the clauses structure of random $k$-SAT problems are expressed as $M \times N$ quenched random matrix where the numbers of ...
- 653
1
vote
1
answer
142
views
Complexity of a satisfiability problem
I would like the know the complexity of a specific satisfiability problem. I have a feeling it could be solved in polynomial time, but I am not sure about it. The problem is described below.
Given $n$ ...
- 13