# Questions tagged [satisfiability]

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

493 questions
Filter by
Sorted by
Tagged with
2 views

40 views

### Is MAX-averageSAT a well-known problem?

Is there any variant of the Boolean SAT or Max-SAT problem that has a flavor of maximizing or minimizing the average of the weights of the satisfied clauses of a WCNF formula? Any literature on an ...
46 views

34 views

30 views

### Reducing Dominant Set Problem to SAT

I am trying to solve a problem and I am really struggling, I would appreciate any help. Given a graph $G$ and an integer $k$ , recognize whether $G$ contains dominating set $X$ with no more than $k$ ...
93 views

### Is Monotone 3-SAT with exactly 3 distinct variables untractable?

I have given the following SAT variation: Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated....
103 views

### Why isn't SAT in coNP?

I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?). But I'm missing why the following machine doesn't turing recognize the complementary of SAT: Given a ...
43 views

### MAXSAT using dpll algorithm?

It's possible to return from a dpll algorithm M as maximum for MAX-SAT problem?: I have a sample: https://gist.github.com/davefernig/e670bda722d558817f2ba0e90ebce66f we can modify recurrency to return ...
2k views

### Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
179 views

### Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset

I am working on a problem defined as the following Given a set of $n$ elements called $R \subseteq \mathbb{N} \times \mathbb{N}$ and numbers $Z,G \in \mathbb{N}$, where $Z$ is a measure of our ...
37 views

### Does 2SAT contained in SAT?

Is it true that $2 S A T \subseteq S A T ?$ and in general is $k S A T \subseteq S A T$ where k is any positive integer is true? Thanks.
27 views

I have $m$ equations of the following form: $$x_1+x_2+\cdots+x_n=s,$$ where each variable is either 1 or 0, and the total number of variables is $m\approx3{,}000$. So I’m thinking of modeling each ...
59 views

### Complete resolution rule for 1-in-k SAT

In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal. (A or B or C) and (!A or D ...
169 views

### Counting the number of satisfied models - given mathematical constraints

Question There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...
33 views

### Reference asking: phase transition in SAT

This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate. It has been experimentally observed (e.g. here) that when ...
64 views

### What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
47 views

### When does Gaussian elimination solve exact 1-in-3 SAT?

Terms: A literal is a variable or its negation. A clause is a set of literals. An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
16 views

### Translating running times of $3$-coloring to $k$-$SAT$ complexity

Suppose there is an $O(f(n))$ algorithm for $3$-coloring a graph on $n$ vertices what does it translate to in terms of time complexity for solving $k$-$SAT$ with $m$ clauses?
93 views

27 views

### Names of specific SAT variants

I enjoy reading research on satisfiability, but sometimes it's easier to find relevant information when you know the names of the variants. Example: All the clauses are width 3 and must have ...
67 views

### Turing reducibility of 2 versions of the satisfiability problem

I need help with this problem. There are 2 versions of the satisfiability problem:  decision version: determine whether an arbitrary formula f is satisfiable or not  search ...
64 views

### Reducibility of 2 boolean satisfiability problems

I beg some help with this problem. There are 2 boolean satisfiability problems. Problem $A$: Determining whether an arbitrary formula of size $n$ is $satisfiable$. Problem $B$: Determining ...
57 views

### CircuitSAT to 1-in-3SAT

This question follows Unique 3SAT to Unique 1-in-3SAT Consider an AND gate such that (A ∧ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables.  (A ∨ B ∨ \overline{...
209 views

### Unique 3SAT to Unique 1-in-3SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such ...
30 views

### Unique 1-in-3 SAT

Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment. I know the value of each bit of the unique assignment because it was made from a binary ...
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...