Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more

Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
2 votes
0 answers
30 views

Satisfiability of a boolean formula with two occurrences of each variable with a special ordering

I am interested in the complexity of a special case of the boolean satisfiability problem: We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
SimonNW's user avatar
  • 86
1 vote
2 answers
50 views

Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?

AFAIK, Interior Point method for solving a system of linear inequations is polynomial in the number of variables and constraints. Probably there are others. I don't need to optimize any function (...
Serge Rogatch's user avatar
-1 votes
0 answers
35 views

Showing that $SAT-2 \in P$ [duplicate]

Let $SAT-2$ denote the CNF such that each variable only appears in at most 2 literals. I want to prove that there is a polynomial algorithm for it. I know I have to reduce the problem to finding a ...
Dave the Sid's user avatar
1 vote
1 answer
25 views

Size of circuit generating the solutions of a SAT problem

We have a satisfiable CNF formula $F$ which maps $\{0,1\}^n \to \{0,1\}$. Let us call $S\in \{0,1\}^n$ the set of inputs that satisfy $F$, i.e. $F(s)=1 \, \forall s\in S$. There is a circuit $C$ with $...
Doriano Brogioli's user avatar
0 votes
0 answers
12 views

Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
csaltachin's user avatar
0 votes
0 answers
10 views

Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
Geremia's user avatar
  • 142
0 votes
0 answers
10 views

Check if sum of positive integers is less than a W integer in CNF

As title says, what I am trying to do is to find a way to sum integers and later compare them with another integer W, in a manner that when the sum of integers is less or equal than W, using only CNF. ...
Francisco Jos Rodriguez Rugele's user avatar
0 votes
1 answer
68 views

P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph

The picture below shows how to reduce the Boolean Satisfiability problem in CNF to the circulation problem in undirected graph (see here). As you can see, a[i] are ...
Serge Rogatch's user avatar
3 votes
1 answer
33 views

Is boolean formula equivalence problem for 2-CNFs $\mathsf{coNP}$-hard?

The problem: Given two boolean formulas in 2-CNF, decide if they are equivalent. I know that the problem is $\mathsf{coNP}$-hard when at least one formula is in 3-CNF. However, the same proof of $\...
rus9384's user avatar
  • 1,654
0 votes
2 answers
37 views

how to polynomially check if a given boolean formula is unsatisfiable

Since SAT is np-complete, there is a polynomial algorithm to check if a given solution for any particular formula is correct. Just substitute the values and solve. But what if one claims that the ...
Alex Matyasaur's user avatar
4 votes
1 answer
203 views

Tseitin formula on 2-connected graph

How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
David's user avatar
  • 1
1 vote
1 answer
129 views

Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
A. H.'s user avatar
  • 498
1 vote
1 answer
145 views

SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples? I mean implementations more efficient than the naive approach, i.e. each ...
Fabius Wiesner's user avatar
1 vote
0 answers
90 views

Sat solvers with backdoor set

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I ...
Alexey Kholodkov's user avatar
2 votes
0 answers
71 views

Monotone boolean satisfiability problem : finding minimal solutions

I am very interested in the following questions, which sprang out from the topological study of loops in surfaces and their intersection numbers. Consider, over a finite set of boolean variables $X$, ...
Christopher-Lloyd Simon's user avatar
1 vote
1 answer
322 views

How fast can we make generalized k-SAT?

Suppose a generalized version of k-SAT where the usual clauses (disjunctions of literals) are generalized to arbitrary Boolean functions of k variables. (For example, $(x \oplus (y \land z)), ((x \...
A. H.'s user avatar
  • 498
4 votes
1 answer
193 views

SAT formulation of the condition that an even number of a given set of variables must be set to true

Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course ...
Sander's user avatar
  • 203
2 votes
2 answers
848 views

How to find a satisfying assignment in polynomial time without the use of randomness?

Assume that we are given a formula in 3-CNF such that at least 1% of the complete assignments satisfy it. My question is how to find a satisfying assignment in polynomial time without the use of ...
S. M.'s user avatar
  • 317
1 vote
1 answer
43 views

Is it possible to find reductions from problems in $\mathsf{NP}$ to SAT based solely on the certificate verification algorithm?

The following problem has made me ask this question: Given a boolean formula $\varphi(X)$ decide if there exists a quantification of $\varphi(X)$ with $k$ $\forall$ quantifiers that holds true. ...
rus9384's user avatar
  • 1,654
1 vote
0 answers
22 views

CNF Horn-renamability to 3-CNF Horn-renamability reduction?

A CNF formula is Horn-renamable if you can invert variables in such a way that each clause has at most one positive literal. There is an algorithm based on a reduction to 2-SAT given in Renaming a Set ...
rus9384's user avatar
  • 1,654
1 vote
1 answer
114 views

Reduce CNF-SAT to decision problem

Given CNF-SAT reduce it to the following decision problem: Given n items, m groups (and for each group a set of items) and a ...
popcorn's user avatar
  • 183
0 votes
0 answers
16 views

Does $\mathsf{NC_1\subsetneq NC}$ imply $\mathsf{NP\neq coNP}$?

Any $\mathsf{NC}$ circuit could be presented in SAT form via Tseytin transform. This applies in the reverse too: an arbitrary SAT instance could encode any $\mathsf{NC}$ circuit. Now, Frege proof ...
rus9384's user avatar
  • 1,654
0 votes
0 answers
70 views

The parameterized complexity of Weighted-CNF-SAT parameterized by the number of clauses

What is the parameterized complexity of Weighted-CNF-SAT, when parameterized by the number of clauses? Input: A CNF formula $\phi$ with $m$ clauses and $n$ variables, and an integer $k$. Parameter: $m$...
user3445340's user avatar
0 votes
0 answers
28 views

Is it possible to perform clause-pair minimization on a CNF instance in $o(n^2)$ time?

Let $\varphi(X)$ be a boolean formula in CNF over a set $X$ of boolean variables $x_1,x_2,...,x_n$. Let $c_i$ denote $i^{th}$ clause in $\varphi(X)$. $x_j^0$ denotes $\overline{x_j}$ and $x_j^1$ ...
rus9384's user avatar
  • 1,654
1 vote
0 answers
24 views

Are there any SAT outside of $\mathsf{RP}$ variants that are solvable in quasipolynomial time?

It's possible to construct SAT problems that are solvable in quasipolynomial time, but they are also solvable in polylogarithmic space. Consider, for example, the following problem: Let a set $S$ ...
rus9384's user avatar
  • 1,654
1 vote
0 answers
22 views

SAT for clauses of the form "At most m out of n are false"

Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then: A ...
Jim's user avatar
  • 111
0 votes
0 answers
25 views

Computational Learning Problem: 3-DNF Reduction

I'm not sure how to solve this problem. Problem statement is: Consider the binary classification problem where X = R d and Y = {0, 1}. Consider the class of Binary classifiers given by intersection of ...
Mr.Zhang's user avatar
1 vote
2 answers
59 views

Complexity of satisfiability for relational logic on the booleans

I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
user1868607's user avatar
  • 2,194
1 vote
1 answer
140 views

How to find the learned clause from a UIP cut

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm. In implementing CDCL, I read ...
Jack Sack's user avatar
0 votes
1 answer
21 views

How does the sumcheck protocol help solving the #SAT (circuit satisfiability) problem?

I am going through Justin Thaler's book - https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf - "Proofs, Arguments, and Zero-Knowledge" He presents the Sumcheck protocol & then ...
user93353's user avatar
  • 125
0 votes
0 answers
34 views

Number of clauses in SAT problems

I was going through the proof that DNF-SAT can be solved in polynomial time. The strategy was to go through all clauses, find a clause that doesn't contain both x and x' for any variable x and then ...
Aditya's user avatar
  • 1
1 vote
1 answer
103 views

Specialized SAT solver (?)

(Context) Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way. If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
fuzzypixelz's user avatar
0 votes
0 answers
33 views

Does the following down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"?

Does the following highly down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"? If not, why not? Marek, V. Wiktor. Introduction to Mathematics of ...
Geremia's user avatar
  • 142
0 votes
2 answers
75 views

Can any SAT problem be converted to a system of linear equations over $\mathbf{Z}_2$?

Can any SAT problem be converted into one with only affine formulas? Handbook of Satisfiability p. 672: Affine formulas. A linear equation over the two-element field is an expression of the form $x_1 ...
Geremia's user avatar
  • 142
0 votes
3 answers
85 views

Is there a 2SAT encoding for a NAND gate

I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
Hovercraft2's user avatar
1 vote
1 answer
89 views

A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?

I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster. My implementation ...
Tilo RC's user avatar
  • 11
0 votes
0 answers
13 views

Reference request for Unit Clause Based SAT Reduction Rules

I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My ...
Russell Easterly's user avatar
0 votes
0 answers
24 views

Reduction of $3SAT$ to $2P2N-3SAT$ (without trivial clauses)

Given an instance of $3SAT$ the objective is to reduce it directly to $2P2N-3SAT$ without the reduction having any 'trivial' clauses. The trivial clauses can be where the same variable in a clause is ...
J.Doe's user avatar
  • 789
4 votes
2 answers
108 views

Finding a vector of maximum Hamming distance from a subspace of $(\mathbb{Z}/2\mathbb{Z})^n$

Let $W$ be a linear subspace of the vector space $V = (\mathbb{Z}/2\mathbb{Z})^n$. Let $k = \dim(W)$. For $v \in V$, define the distance from $v$ to $W$ to be $d(v,W):=\min_{w\in W} d(v,w)$ where $d(...
Ben's user avatar
  • 141
0 votes
1 answer
86 views

Is it an open problem if CDCL algorithms violate SETH?

Strong Exponential Time Hypothesis states that general SAT, where clauses are not limited in length, can't be solved in time $o(2^n)$. It's proven that DPLL algorithm requires $\Omega(2^n)$ time in ...
rus9384's user avatar
  • 1,654
-1 votes
1 answer
44 views

Schaefer's dichotomy theorem and limits on the formula length

Schaefer's dichotomy theorem ensures than when a constraint satisfiability problem satisfies certain conditions, the problem is either in $\mathsf P$ or is $\mathsf{NP}$-hard. Suppose the following ...
rus9384's user avatar
  • 1,654
1 vote
0 answers
41 views

Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?

Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
Soha's user avatar
  • 25
0 votes
0 answers
68 views

if it were shown that every algorithm that solves SAT must have complexity Ω(n^(log n)) then P≠NP?

Shouldn't this statement be false? To be true the implication should be P=NP or am I wrong? I can't find a formal proof
PatrickBateman's user avatar
0 votes
0 answers
17 views

Complexity Class of the Problem: Existence of Unsatisfying Interpretations in Boolean Formulas

What is the complexity class of the problem if there exist two different interpretations that do not satisfy a given Boolean formula? I believe the problem of existence of an interpretation that does ...
Lupital's user avatar
0 votes
1 answer
501 views

Complexity of a variant of #Positive-2-SAT

#Positive-2SAT is the problem of counting the number of satisfying assignments to a given Positive 2-CNF formula i.e 2-CNF formulas in which each literal is a positive occurrence of a variable. The ...
Anuj's user avatar
  • 41
1 vote
1 answer
170 views

Why is conjunctive normal form (CNF) "better" for SAT than disjunctive normal form (DNF)?

When hand-manipulating algebra DNF (sum of products) is easier than CNF (product of sums). Possibly because factoring is more difficult than expanding. So why is it the opposite for computational ...
Gaslight Deceive Subvert's user avatar
0 votes
1 answer
46 views

Should I remove equivalent variables in a CNF file to be used by a SAT solver?

My CNF file ends with many pairs of clauses that represent that two variables are equivalent (eg: -3 7, 3 -7, 5 -11, -5 11, etc.). Do most SAT solvers automatically pre-process these and replace every ...
Lewis Baxter's user avatar
0 votes
1 answer
85 views

How to solve boolean SAT with equality constraints

Say I have boolean formula in form of a CNF(x1,x2,...) with $x_i$ being boolean variables. Testing the satisfiability of the CNF is the SAT problem, i.e. determine ...
Andreas H.'s user avatar
0 votes
0 answers
73 views

Finding a Polynomial Time algorithm for the 3-SAT Problem

Let us consider m clauses containing 3 variables each i.e. A1,A2,A3...Am . Let the total literals in consideration be n. Then each clause : Ai = (xr $\lor$ xs $\lor$ xt) where 1 $\le$ r,s,t $\le$n and ...
Pathlessbark8's user avatar
-1 votes
1 answer
106 views

SAT polynomial time

Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
Jip Helsen's user avatar

1
2 3 4 5
14