liu.seSearch for publications in DiVA

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt152",{id:"formSmash:upper:j_idt152",widgetVar:"widget_formSmash_upper_j_idt152",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt153_j_idt155",{id:"formSmash:upper:j_idt153:j_idt155",widgetVar:"widget_formSmash_upper_j_idt153_j_idt155",target:"formSmash:upper:j_idt153:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Algorithms, measures and upper bounds for satisfiability and related problemsPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2007 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Linköping, Sweden: Department of Computer and Information Science, Linköpings universitet , 2007. , 234 p.
##### Series

Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1079
##### Keyword [en]

Exact algorithms, upper bounds, algorithm analysis, satisfiability
##### National Category

Computer Science
##### Identifiers

URN: urn:nbn:se:liu:diva-8714ISBN: 978-91-85715-55-8OAI: oai:DiVA.org:liu-8714DiVA: diva2:23420
##### Public defence

2007-04-27, Visionen, B-huset, Linköpings universitet, Linköping, 13:15 (English)
##### Opponent

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt400",{id:"formSmash:j_idt400",widgetVar:"widget_formSmash_j_idt400",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt406",{id:"formSmash:j_idt406",widgetVar:"widget_formSmash_j_idt406",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt413",{id:"formSmash:j_idt413",widgetVar:"widget_formSmash_j_idt413",multiple:true});
Available from: 2007-04-16 Created: 2007-04-16 Last updated: 2014-04-24
##### List of papers

The topic of exact, exponential-time algorithms for NP-hard problems has received a lot of attention, particularly with the focus of producing algorithms with stronger theoretical guarantees, e.g. upper bounds on the running time on the form O(c^n) for some c. Better methods of analysis may have an impact not only on these bounds, but on the nature of the algorithms as well.

The most classic method of analysis of the running time of DPLL-style ("branching" or "backtracking") recursive algorithms consists of counting the number of variables that the algorithm removes at every step. Notable improvements include Kullmann's work on complexity measures, and Eppstein's work on solving multivariate recurrences through quasiconvex analysis. Still, one limitation that remains in Eppstein's framework is that it is difficult to introduce (non-trivial) restrictions on the applicability of a possible recursion.

We introduce two new kinds of complexity measures, representing two ways to add such restrictions on applicability to the analysis. In the first measure, the execution of the algorithm is viewed as moving between a finite set of states (such as the presence or absence of certain structures or properties), where the current state decides which branchings are applicable, and each branch of a branching contains information about the resultant state. In the second measure, it is instead the relative sizes of the modelled attributes (such as the average degree or other concepts of density) that controls the applicability of branchings.

We adapt both measures to Eppstein's framework, and use these tools to provide algorithms with stronger bounds for a number of problems. The problems we treat are satisfiability for sparse formulae, exact 3-satisfiability, 3-hitting set, and counting models for 2- and 3-satisfiability formulae, and in every case the bound we prove is stronger than previously known bounds.

1. Counting Satisfying Assignments in 2-SAT and 3-SAT$(function(){PrimeFaces.cw("OverlayPanel","overlay23415",{id:"formSmash:j_idt449:0:j_idt453",widgetVar:"overlay23415",target:"formSmash:j_idt449:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. Exact algorithms for finding minimum transversals in rank-3 hypergraphs$(function(){PrimeFaces.cw("OverlayPanel","overlay23416",{id:"formSmash:j_idt449:1:j_idt453",widgetVar:"overlay23416",target:"formSmash:j_idt449:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. Counting models for 2sat and 3sat formulae$(function(){PrimeFaces.cw("OverlayPanel","overlay23417",{id:"formSmash:j_idt449:2:j_idt453",widgetVar:"overlay23417",target:"formSmash:j_idt449:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. Faster exact solving of SAT formulae with a low number of occurrences per variable$(function(){PrimeFaces.cw("OverlayPanel","overlay23418",{id:"formSmash:j_idt449:3:j_idt453",widgetVar:"overlay23418",target:"formSmash:j_idt449:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. An algorithm for the sat problem for formulae of linear length$(function(){PrimeFaces.cw("OverlayPanel","overlay23419",{id:"formSmash:j_idt449:4:j_idt453",widgetVar:"overlay23419",target:"formSmash:j_idt449:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1144",{id:"formSmash:lower:j_idt1144",widgetVar:"widget_formSmash_lower_j_idt1144",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1145_j_idt1147",{id:"formSmash:lower:j_idt1145:j_idt1147",widgetVar:"widget_formSmash_lower_j_idt1145_j_idt1147",target:"formSmash:lower:j_idt1145:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});