Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
694
questions
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 ...
- 163
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 ...
- 163
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
Negating a Quantified Boolean Formula (QBF)
I'm reading about quantified boolean formulas. One sentence mentions:
You should also verify that the negation of the formula $Q_1x_1\cdot\cdot\cdot Q_nx_n \phi(x_1, ..., x_n)$ is the same as $Q^{\...
- 141
1
vote
0
answers
18
views
"package" compatibility solver with verion ranges
I am looking for how to solve the package compatibility problem. I have found some relevant research and libraries. But some of them are older. I am wondering if there is any more recent research and ...
- 111
2
votes
0
answers
38
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 ...
- 160
1
vote
2
answers
56
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 (...
- 155
1
vote
1
answer
27
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 $...
- 145
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 ...
- 155
3
votes
1
answer
38
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 $\...
- 1,966
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 ...
4
votes
1
answer
217
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 ...
- 1
1
vote
1
answer
134
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 ...
- 593
2
votes
1
answer
195
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 ...
- 135
1
vote
0
answers
92
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 ...
- 123
2
votes
0
answers
87
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$, ...
1
vote
1
answer
330
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 \...
- 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$...
- 31
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
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 ...
- 43
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
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