Questions tagged [sat]

SAT stands for the Boolean satisfiability problem.

Filter by
Sorted by
Tagged with
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 ...
Russell Easterly's user avatar
-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 ...
Jxb's user avatar
  • 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 ...
Jxb's user avatar
  • 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\...
Junqiang Peng's user avatar
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 ...
Noel Arteche's user avatar
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 ...
Jova's user avatar
  • 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 ...
Jxb's user avatar
  • 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 ...
a3nm's user avatar
  • 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?
Jxb's user avatar
  • 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,...
Amar Shah's user avatar
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 ...
rus9384's user avatar
  • 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 ...
Noel Arteche's user avatar
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.) ...
Inspired_Blue's user avatar
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)},\ \...
Soham Chatterjee's user avatar
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 ...
Jxb's user avatar
  • 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 ...
Denis's user avatar
  • 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: $$ \...
Nicola Gigante's user avatar
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 ...
Jxb's user avatar
  • 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. ...
wtfamidoing's user avatar
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, ...
hddmss's user avatar
  • 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 ...
Nicola Gigante's user avatar
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 ...
Charles's user avatar
  • 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, ...
vinaych's user avatar
  • 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 ...
gdoug's user avatar
  • 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 ...
user67418's user avatar
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 ...
LLL's user avatar
  • 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 ...
DanielM's user avatar
  • 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 ...
Russell Easterly's user avatar
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 ...
hellothere's user avatar
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 ...
Xavier Labouze's user avatar
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\...
Amritanshu singh's user avatar
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 ...
zhukui bai's user avatar
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)$...
David Monniaux's user avatar
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 ...
J.Doe's user avatar
  • 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 ...
TheoryQuest1's user avatar
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 ...
Craig's user avatar
  • 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 ...
Timothy Schommer's user avatar
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 ...
ferris's user avatar
  • 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 ...
Shuxue Jiaoshou's user avatar
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 ...
hddmss's user avatar
  • 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 ...
user63167's user avatar
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. "...
Omar Shehab's user avatar
-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 ...
gust's user avatar
  • 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 ...
Giang Trinh's user avatar
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?
Omar Shehab's user avatar
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 ? ...
SagarM's user avatar
  • 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 ...
SagarM's user avatar
  • 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 $...
Turbo's user avatar
  • 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 ...
Omar Shehab's user avatar
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$ ...
borroot's user avatar
  • 13

1
2 3 4 5
7