Random restarts for unsatisfiable problemsWhat'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
Who are the people reviewing far more papers than they're submitting for review?
Anagrams Question
Permutations in Disguise
Wouldn't Kreacher have been able to escape even without following an order?
What if I don't know whether my program will be linked to a GPL library or not?
Smooth irreducible subvarieties in an algebraic group that are stable under power maps
Why is belonging not transitive?
Why 1.5fill is 0pt
how to know this integral finite or infinite
Persuading players to be less attached to a pre-session 0 character concept
Did slaves have slaves?
Pure python range implementation
Python web-scraper to download table of transistor counts from Wikipedia
Output Distinct Factor Cuboids
What is this WWII four-engine plane on skis?
Can Brexit be undone in an emergency?
How can I draw overlapping triangles?
Hobby function generators
How to choose a power source for Raspberry Pi 4?
Delete empty subfolders, keep parent folder
What does the "capacitor into resistance" symbol mean?
What does “We have long ago paid the goblins of Moria,” from The Hobbit mean?
Floating Point XOR
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 9 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 9 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 9 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 9 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 9 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 9 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 9 hours ago
rwallacerwallace
2191 silver badge8 bronze badges
asked 9 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
