scholarly journals On Irrelevant Literals in Pseudo-Boolean Constraint Learning

2020 ◽  
Author(s):  
Daniel Le Berre ◽  
Pierre Marquis ◽  
Stefan Mengel ◽  
Romain Wallon
Keyword(s):  
Cutting Planes ◽  
Np Hard ◽  
Clause Learning ◽  
Truth Value ◽  
Constraint Learning

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain irrelevant literals, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard).

scholarly journals On Division Versus Saturation in Pseudo-Boolean Solving

2019 ◽  
Author(s):  
Stephan Gocht ◽  
Jakob Nordström ◽  
Amir Yehudayoff
Keyword(s):  
Linear Programming ◽  
Cutting Planes ◽  
The Other ◽  
Sat Solving ◽  
Linear Combinations ◽  
Division Rule ◽  
Clause Learning

The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al., '87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with division instead of saturation can be exponentially stronger. In the other direction, we prove that simulating a single saturation step can require an exponential number of divisions. We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes.

scholarly journals Automating cutting planes is NP-hard

2020 ◽  
Author(s):  
Mika Göös ◽  
Sajin Koroth ◽  
Ian Mertz ◽  
Toniann Pitassi
Keyword(s):  
Cutting Planes ◽  
Np Hard

Chapter 7. Proof Complexity and SAT Solving

2021 ◽  
Author(s):  
Sam Buss ◽  
Jakob Nordström
Keyword(s):  
Linear Algebra ◽  
Cutting Planes ◽  
Proof Complexity ◽  
Sat Solving ◽  
Proof Systems ◽  
Frege Systems ◽  
Ample Supply ◽  
Clause Learning ◽  
Algebraic Approaches ◽  
Polynomial Calculus

This chapter gives an overview of proof complexity and connections to SAT solving, focusing on proof systems such as resolution, Nullstellensatz, polynomial calculus, and cutting planes (corresponding to conflict-driven clause learning, algebraic approaches using linear algebra or Gröbner bases, and pseudo-Boolean solving, respectively). There is also a discussion of extended resolution (which is closely related to DRAT proof logging) and Frege and extended Frege systems more generally. An ample supply of references for further reading is provided, including for some topics omitted in this chapter.

Learning Importance of Preferences

10.29007/v68w ◽  
2018 ◽  
Author(s):  
Ying Zhu ◽  
Mirek Truszczynski
Keyword(s):  
Polynomial Time ◽  
Polynomial Time Algorithm ◽  
Time Algorithm ◽  
Scoring Rules ◽  
Np Hard ◽  
Individual Preferences

We study the problem of learning the importance of preferences in preference profiles in two important cases: when individual preferences are aggregated by the ranked Pareto rule, and when they are aggregated by positional scoring rules. For the ranked Pareto rule, we provide a polynomial-time algorithm that finds a ranking of preferences such that the ranked profile correctly decides all the examples, whenever such a ranking exists. We also show that the problem to learn a ranking maximizing the number of correctly decided examples (also under the ranked Pareto rule) is NP-hard. We obtain similar results for the case of weighted profiles when positional scoring rules are used for aggregation.

How Art Works

2018 ◽  
Author(s):  
Ellen Winner
Keyword(s):  
Statistical Analysis ◽  
Data Collection ◽  
Social Science ◽  
Modern Art ◽  
Hard Work ◽  
Objective Truth ◽  
The Arts ◽  
Art Form ◽  
Art Works ◽  
Truth Value

This book is an examination of what psychologists have discovered about how art works—what it does to us, how we experience art, how we react to it emotionally, how we judge it, and what we learn from it. The questions investigate include the following: What makes us call something art? Do we experience “real” emotions from the arts? Do aesthetic judgments have any objective truth value? Does learning to play music raise a child’s IQ? Is modern art something my kid could do? Is achieving greatness in an art form just a matter of hard work? Philosophers have grappled with these questions for centuries, and laypeople have often puzzled about them too and offered their own views. But now psychologists have begun to explore these questions empirically, and have made many fascinating discoveries using the methods of social science (interviews, experimentation, data collection, statistical analysis).

Internal categoricity and truth

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Lower Order ◽  
Higher Order ◽  
Mathematical Truth ◽  
Object Language ◽  
Famous Result ◽  
Famous Paper ◽  
Truth Value ◽  
Truth Operator

This chapter considers whether internal categoricity can be used to leverage any claims about mathematical truth. We begin by noting that internal categoricity allows us to introduce a truth-operator which gives an object-language expression to the supervaluationist semantics. In this way, the univocity discussed in previous chapters might seem to secure an object-language expression of determinacy of truth-value; but this hope falls short, because such truth-operators must be carefully distinguished from truth-predicates. To introduce these truth-predicates, we outline an internalist attitude towards model theory itself. We then use this to illuminate the cryptic conclusions of Putnam's justly-famous paper ‘Models and Reality’. We close this chapter by presenting Tarski’s famous result that truth for lower-order languages can be defined in higher-order languages.

Probabilities as Truth-Value Estimates

1961 ◽  
Vol 28 (4) ◽  
pp. 414-417
Author(s):  
Hugues Leblanc
Keyword(s):  
Truth Value

scholarly journals Optimizing Transmit Sequence and Instrumental Variables Receiver for Dual-Function Complexity System

Complexity ◽  
2020 ◽  
Vol 2020 ◽  
pp. 1-13
Author(s):  
Yu Yao ◽  
Junhui Zhao ◽  
Lenan Wu
Keyword(s):  
Approximate Solution ◽  
Instrumental Variables ◽  
Performance Index ◽  
Dual Function ◽  
Np Hard ◽  
Match Filter ◽  
Filter Output ◽  
Phase Code ◽  
Discrete Phase ◽  
Simulation Results

This correspondence deals with the joint cognitive design of transmit coded sequences and instrumental variables (IV) receive filter to enhance the performance of a dual-function radar-communication (DFRC) system in the presence of clutter disturbance. The IV receiver can reject clutter more efficiently than the match filter. The signal-to-clutter-and-noise ratio (SCNR) of the IV filter output is viewed as the performance index of the complexity system. We focus on phase only sequences, sharing both a continuous and a discrete phase code and develop optimization algorithms to achieve reasonable pairs of transmit coded sequences and IV receiver that fine approximate the behavior of the optimum SCNR. All iterations involve the solution of NP-hard quadratic fractional problems. The relaxation plus randomization technique is used to find an approximate solution. The complexity, corresponding to the operation of the proposed algorithms, depends on the number of acceptable iterations along with on and the complexity involved in all iterations. Simulation results are offered to evaluate the performance generated by the proposed scheme.

On the Complexity of Deadlock Recovery

1986 ◽  
Vol 9 (3) ◽  
pp. 323-342
Author(s):  
Joseph Y.-T. Leung ◽  
Burkhard Monien
Keyword(s):  
Computational Complexity ◽  
Polynomial Time ◽  
Arbitrary Number ◽  
The Other ◽  
Np Hard ◽  
Total Cost ◽  
Other Hand ◽  
Input Parameters ◽  
Resource Type

We consider the computational complexity of finding an optimal deadlock recovery. It is known that for an arbitrary number of resource types the problem is NP-hard even when the total cost of deadlocked jobs and the total number of resource units are “small” relative to the number of deadlocked jobs. It is also known that for one resource type the problem is NP-hard when the total cost of deadlocked jobs and the total number of resource units are “large” relative to the number of deadlocked jobs. In this paper we show that for one resource type the problem is solvable in polynomial time when the total cost of deadlocked jobs or the total number of resource units is “small” relative to the number of deadlocked jobs. For fixed m ⩾ 2 resource types, we show that the problem is solvable in polynomial time when the total number of resource units is “small” relative to the number of deadlocked jobs. On the other hand, when the total number of resource units is “large”, the problem becomes NP-hard even when the total cost of deadlocked jobs is “small” relative to the number of deadlocked jobs. The results in the paper, together with previous known ones, give a complete delineation of the complexity of this problem under various assumptions of the input parameters.

Sign in / Sign up

Export Citation Format

Share Document