Skip to main content

# Questions tagged [satisfiability]

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

694 questions
Filter by
Sorted by
Tagged with
0 votes
1 answer
26 views

### Identifying Variables That Are Always False in Horn-SAT and Enumerating All Solutions

I am studying the satisfiability problem for Horn-SAT and trying to understand how to efficiently identify variables that are always false across all possible solutions. Additionally, I am interested ...
0 votes
1 answer
45 views

### Can we use XOR's forced branching to show that NP!=P

Backstory: As happens, every now and then, one encounters an idea, prompting the question: Could I use this to prove that NP==P, or vice versa NP!=P So then, today I got to trying to show that NP!=P ...
• 15
1 vote
1 answer
38 views

### Is Monotone Not-Exactly-1 3SAT solvable in polynomial time?

I'm studying different variants of the SAT problem, and I came across the Monotone Not-Exactly-1 3SAT problem. Specifically, this problem involves determining whether a Boolean formula in CNF, where ...
2 votes
1 answer
29 views

### Are all solutions to a HORN-SAT problem required to contain the minimal model as a subset?

I'm studying HORN-SAT problems and I have a specific question about the minimal model. Given a HORN-SAT problem with multiple solutions, I understand that the minimal model is the one with the ...
2 votes
1 answer
90 views

### Counting number of assignments restricted by implications

Suppose we have $n$ boolean variables, $x_1, \dots, x_n$. Some boolean variables can have implication relationships, e.g. $x_2 \implies x_5$, which means that if $x_2$ is true $x_5$ must also be true. ...
• 13.8k
0 votes
0 answers
35 views

### Minimum unsat core and generalization

I have a problem that has been in my head for some time, it might be already well known but i cannot find ressources on something similar : The idea came from the will to identify the minimal unsat ...
4 votes
1 answer
372 views

### Is 3, 3 satisfiability trivial after all?

Tovey's paper from 1982 clearly states that: Theorem 2.1. Boolean satisfiability is NP-complete when restricted to instances with 2 or 3 variables per clause and at most 3 occurrences per variable. ...
1 vote
1 answer
27 views

### Is stable infinity required of theories combined with model-based theory combination?

In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen ...
1 vote
2 answers
43 views

### Do stably-infinite theories exclude finite sorts?

Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
3 votes
1 answer
50 views

### File format for SAT competitions

The file format for SAT competitions is available online here: Rules of the 2011 SAT Competition but is defacto inaccessible because all browsers redirect to the non-existing address. Question: where ...
• 143
2 votes
1 answer
28 views

### Limited constant degree HamCycle

Let $G=(V,E)$ be a directed graph. I am interested in a "relaxed" version of the HamCycle problem. In my first case, the degree of each vertex is exactly 6, such that: 3 are outgoing edges ...
• 485
2 votes
1 answer
68 views

### 1-in-k-SAT problem restricted to only positive literals and at most two occurrences of a variable

1-in-k-SAT problem is to determine if there’s an assignment to variables such that every clause has exactly one true literal. Is this problem known to be in P when restricted to positive literals, and ...
• 23
1 vote
1 answer
51 views

### Applications of a SAT Solver Oracle for Determining the Uniqueness of Solutions

I am exploring two kinds of model $𝑝_{𝑚,𝑛,k}$ and $S_{m,n,k}$ within the realm of satisfiability problems (SAT). Formal construction of $𝑝_{𝑚,𝑛,k}$ To construct the $𝑝_{𝑚,𝑛,k}$ model in ...
• 390
0 votes
1 answer
92 views

0 votes
0 answers
18 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 ...
1 vote
0 answers
19 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?
• 154
0 votes
0 answers
14 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. ...
0 votes
1 answer
78 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 ...
3 votes
1 answer
38 views

• 593
4 votes
1 answer
199 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 ...
• 225
3 votes
2 answers
893 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 ...
• 344
1 vote
1 answer
44 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. ...
• 1,966
1 vote
0 answers
24 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 ...
• 1,966
1 vote
1 answer
119 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 ...
• 183
0 votes
0 answers
17 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 ...
• 1,966
0 votes
0 answers
95 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$...
0 votes
0 answers
29 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$ ...
• 1,966
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$ ...
• 1,966
2 votes
0 answers
23 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 ...
• 171
0 votes
0 answers
27 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 ...
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 ...
• 2,204
1 vote
1 answer
211 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 ...
0 votes
1 answer
24 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 ...
• 125
0 votes
0 answers
35 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 ...
1 vote
1 answer
109 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)$ ...
• 145
0 votes
0 answers
35 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 ...
• 154
0 votes
2 answers
106 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 ...
• 154
0 votes
3 answers
90 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?
2 votes
1 answer
105 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 ...
• 21