Random restarts for unsatisfiable problemsWhat's an example of an unsatisfiable 3-CNF formula?Sound and...
Have you ever been issued a passport or national identity card for travel by any other country?
Beauville-Laszlo for schemes
Did slaves have slaves?
How To Make Earth's Oceans as Brackish as Lyr's
Pure python range implementation
Which version of the Pigeonhole principle is correct? One is far stronger than the other
Travel distance across water in early prehistory
Other than good shoes and a stick, what are some ways to preserve your knees on long hikes?
How to make classical firearms effective on space habitats despite the coriolis effect?
Are lay articles good enough to be the main source of information for PhD research?
Why does an orbit become hyperbolic when total orbital energy is positive?
In what sequence should an advanced civilization teach technology to medieval society to maximize rate of adoption?
Very lazy puppy
Does household ovens ventilate heat to the outdoors?
Permutations in Disguise
Amortized Loans seem to benefit the bank more than the customer
What's the benefit of prohibiting the use of techniques/language constructs that have not been taught?
Did Sauron ever betray Morgoth?
Can a business put whatever they want into a contract?
Asked to Not Use Transactions and to Use A Workaround to Simulate One
Why is the year in this ISO timestamp not 2019?
Why 1.5fill is 0pt
How would you translate Evangelii Nuntiandi?
Why does dd not make working bootable USB sticks for Microsoft?
Random restarts for unsatisfiable problems
What's an example of an unsatisfiable 3-CNF formula?Sound and complete algorithms for boolean satifiabilityCommon method for solving satisfiability problems which lie in PWhy don't modern SAT solvers use the notion of a “watched clause”, in the same way they use the notion of a “watched literal”?Assignment to make formula unsatisfiableThe Space of an Unsatisfiable FormulaResults on the difficulty of specific random 3-SAT problems?How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?Randomized algorithm for 3SAT
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ margin-bottom:0;
}
$begingroup$
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.
The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).
Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?
satisfiability randomized-algorithms 3-sat sat-solvers
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
$endgroup$
add a comment
|
$begingroup$
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.
The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).
Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?
satisfiability randomized-algorithms 3-sat sat-solvers
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
$endgroup$
add a comment
|
$begingroup$
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.
The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).
Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?
satisfiability randomized-algorithms 3-sat sat-solvers
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
$endgroup$
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.
The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).
Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?
satisfiability randomized-algorithms 3-sat sat-solvers
satisfiability randomized-algorithms 3-sat sat-solvers
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 8 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
2191 silver badge8 bronze badges
add a comment
|
add a comment
|
1 Answer
1
active
oldest
votes
$begingroup$
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
$endgroup$
add a comment
|
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "419"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/4.0/"u003ecc by-sa 4.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f114780%2frandom-restarts-for-unsatisfiable-problems%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
$endgroup$
add a comment
|
$begingroup$
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
$endgroup$
add a comment
|
$begingroup$
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
$endgroup$
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
answered 5 hours ago
Kyle JonesKyle Jones
6,0271 gold badge19 silver badges41 bronze badges
6,0271 gold badge19 silver badges41 bronze badges
add a comment
|
add a comment
|
Thanks for contributing an answer to Computer Science Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f114780%2frandom-restarts-for-unsatisfiable-problems%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
